:: COMPLEX1 semantic presentation

REAL is non zero V33() V34() V35() V39() set
NAT is V33() V34() V35() V36() V37() V38() V39() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non zero V33() V39() set
0 is zero natural complex real ext-real non positive non negative V33() V34() V35() V36() V37() V38() V39() Element of NAT

1 is non zero natural complex real ext-real positive non negative V33() V34() V35() V36() V37() V38() Element of NAT

0 is zero V33() V34() V35() V36() V37() V38() V39() set
{0,1} is non zero set
Funcs ({0,1},REAL) is non zero FUNCTION_DOMAIN of {0,1}, REAL
{ b1 where b1 is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of Funcs ({0,1},REAL) : b1 . 1 = 0 } is set
(Funcs ({0,1},REAL)) \ { b1 where b1 is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of Funcs ({0,1},REAL) : b1 . 1 = 0 } is Element of K19((Funcs ({0,1},REAL)))
K19((Funcs ({0,1},REAL))) is set
K15(((Funcs ({0,1},REAL)) \ { b1 where b1 is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of Funcs ({0,1},REAL) : b1 . 1 = 0 } ),REAL) is non zero set

(0,1) --> (0,1) is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of K19(K20({0,1},REAL))
{0,1} is non zero V33() V34() V35() V36() V37() V38() set
K20({0,1},REAL) is set
K19(K20({0,1},REAL)) is set
2 is non zero natural complex real ext-real positive non negative V33() V34() V35() V36() V37() V38() Element of NAT

(a ^2) + (b ^2) is complex real ext-real set

(a ^2) + (b ^2) is complex real ext-real set
a is complex set
K20(2,REAL) is set
K19(K20(2,REAL)) is set
Funcs (2,REAL) is non zero FUNCTION_DOMAIN of 2, REAL
{ b1 where b1 is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of Funcs (2,REAL) : b1 . 1 = 0 } is set
(Funcs (2,REAL)) \ { b1 where b1 is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of Funcs (2,REAL) : b1 . 1 = 0 } is Element of K19((Funcs (2,REAL)))
K19((Funcs (2,REAL))) is set

b . 0 is set
b is set
c is set

d is set
i2 . 0 is set

i1 is set
y2 . 0 is set
Funcs (2,REAL) is non zero FUNCTION_DOMAIN of 2, REAL
{ b1 where b1 is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of Funcs (2,REAL) : b1 . 1 = 0 } is set
(Funcs (2,REAL)) \ { b1 where b1 is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of Funcs (2,REAL) : b1 . 1 = 0 } is Element of K19((Funcs (2,REAL)))
K19((Funcs (2,REAL))) is set

b . 1 is set
b is set
c is set

d is set
i2 . 1 is set

i1 is set
y2 . 1 is set
a is complex set
(a) is set

b . 0 is set
(a) is set

b . 1 is set
a is complex set
(a) is complex real ext-real set
(a) is complex real ext-real set

a . 0 is set
a . 1 is set

(0,1) --> (b,c) is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of K19(K20({0,1},REAL))
dom a is set

[*a,b*] is complex Element of COMPLEX
([*a,b*]) is complex real ext-real Element of REAL
([*a,b*]) is complex real ext-real Element of REAL

(0,1) --> (c,d) is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of K19(K20({0,1},REAL))

i1 . 0 is set

(0,1) --> (c,d) is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of K19(K20({0,1},REAL))

i1 . 1 is set
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
[*(a),(a)*] is complex Element of COMPLEX

b . 1 is set

(0,1) --> (b,c) is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of K19(K20({0,1},REAL))
Funcs (2,REAL) is non zero FUNCTION_DOMAIN of 2, REAL
{ b1 where b1 is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of Funcs (2,REAL) : b1 . 1 = 0 } is set
(Funcs (2,REAL)) \ { b1 where b1 is Relation-like 2 -defined REAL -valued Function-like quasi_total Element of Funcs (2,REAL) : b1 . 1 = 0 } is Element of K19((Funcs (2,REAL)))
K19((Funcs (2,REAL))) is set

d . 1 is set

i1 . 0 is set

i1 . 1 is set
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
(b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
[*(b),(b)*] is complex Element of COMPLEX
a is complex set
b is complex set
(a) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
() is complex Element of COMPLEX

a is complex set
(a) is complex real ext-real Element of REAL

(a) * (a) is complex real ext-real set
(a) is complex real ext-real Element of REAL

(a) * (a) is complex real ext-real set
((a) ^2) + ((a) ^2) is complex real ext-real Element of REAL
(()) is complex real ext-real Element of REAL
(()) is complex real ext-real Element of REAL
() is complex Element of COMPLEX

(()) is complex real ext-real Element of REAL
(()) is complex real ext-real Element of REAL

[*b,c*] is complex Element of COMPLEX
(0,1) --> (b,c) is Relation-like {0,1} -defined REAL -valued Function-like quasi_total Element of K19(K20({0,1},REAL))

+ (a,b) is complex real ext-real Element of REAL

[*i1,i2*] is complex Element of COMPLEX

[*y2,y2*] is complex Element of COMPLEX
+ (i1,y2) is complex real ext-real Element of REAL
+ (i2,y2) is complex real ext-real Element of REAL
[*(+ (i1,y2)),(+ (i2,y2))*] is complex Element of COMPLEX

+ (a,(opp a)) is complex real ext-real Element of REAL
a + (opp a) is complex real ext-real Element of REAL

* (a,b) is complex real ext-real Element of REAL

[*i1,i2*] is complex Element of COMPLEX

[*y2,y2*] is complex Element of COMPLEX
* (i1,y2) is complex real ext-real Element of REAL
* (i2,y2) is complex real ext-real Element of REAL
opp (* (i2,y2)) is complex real ext-real Element of REAL
+ ((* (i1,y2)),(opp (* (i2,y2)))) is complex real ext-real Element of REAL
* (i1,y2) is complex real ext-real Element of REAL
* (i2,y2) is complex real ext-real Element of REAL
+ ((* (i1,y2)),(* (i2,y2))) is complex real ext-real Element of REAL
[*(+ ((* (i1,y2)),(opp (* (i2,y2))))),(+ ((* (i1,y2)),(* (i2,y2))))*] is complex Element of COMPLEX

* ((opp i2),y2) is complex real ext-real Element of REAL
+ ((* (i1,y2)),(* ((opp i2),y2))) is complex real ext-real Element of REAL
c is complex set
a is complex set
b is complex set
a + b is complex set
(c) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL

[*d,i1*] is complex Element of COMPLEX

[*i2,y2*] is complex Element of COMPLEX
+ (d,i2) is complex real ext-real Element of REAL
+ (i1,y2) is complex real ext-real Element of REAL
[*(+ (d,i2)),(+ (i1,y2))*] is complex Element of COMPLEX
c is complex set
a is complex set
b is complex set
a + b is complex set
(c) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL

[*d,i1*] is complex Element of COMPLEX

[*i2,y2*] is complex Element of COMPLEX
+ (d,i2) is complex real ext-real Element of REAL
+ (i1,y2) is complex real ext-real Element of REAL
[*(+ (d,i2)),(+ (i1,y2))*] is complex Element of COMPLEX
c is complex set
a is complex set
b is complex set
a * b is complex set
(c) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL

[*d,i1*] is complex Element of COMPLEX

[*i2,y2*] is complex Element of COMPLEX
* (d,i2) is complex real ext-real Element of REAL
* (i1,y2) is complex real ext-real Element of REAL
opp (* (i1,y2)) is complex real ext-real Element of REAL
+ ((* (d,i2)),(opp (* (i1,y2)))) is complex real ext-real Element of REAL
* (d,y2) is complex real ext-real Element of REAL
* (i1,i2) is complex real ext-real Element of REAL
+ ((* (d,y2)),(* (i1,i2))) is complex real ext-real Element of REAL
[*(+ ((* (d,i2)),(opp (* (i1,y2))))),(+ ((* (d,y2)),(* (i1,i2))))*] is complex Element of COMPLEX
(* (d,i2)) + (opp (* (i1,y2))) is complex real ext-real Element of REAL

(d * i2) + (opp (* (i1,y2))) is complex real ext-real Element of REAL
- (* (i1,y2)) is complex real ext-real Element of REAL
(d * i2) + (- (* (i1,y2))) is complex real ext-real Element of REAL
(d * i2) - (* (i1,y2)) is complex real ext-real Element of REAL
c is complex set
a is complex set
b is complex set
a * b is complex set
(c) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) + ((a) * (b)) is complex real ext-real Element of REAL

[*d,i1*] is complex Element of COMPLEX

[*i2,y2*] is complex Element of COMPLEX
* (d,i2) is complex real ext-real Element of REAL
* (i1,y2) is complex real ext-real Element of REAL
opp (* (i1,y2)) is complex real ext-real Element of REAL
+ ((* (d,i2)),(opp (* (i1,y2)))) is complex real ext-real Element of REAL
* (d,y2) is complex real ext-real Element of REAL
* (i1,i2) is complex real ext-real Element of REAL
+ ((* (d,y2)),(* (i1,i2))) is complex real ext-real Element of REAL
[*(+ ((* (d,i2)),(opp (* (i1,y2))))),(+ ((* (d,y2)),(* (i1,i2))))*] is complex Element of COMPLEX
(* (d,y2)) + (* (i1,i2)) is complex real ext-real Element of REAL

(d * y2) + (* (i1,i2)) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
a + b is complex set
(b) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL
[*((a) + (b)),((a) + (b))*] is complex Element of COMPLEX
([*((a) + (b)),((a) + (b))*]) is complex real ext-real Element of REAL

(d) is complex real ext-real Element of REAL
([*((a) + (b)),((a) + (b))*]) is complex real ext-real Element of REAL
(d) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
a * b is complex set
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
((a) * (b)) + ((b) * (a)) is complex real ext-real Element of REAL
[*(((a) * (b)) - ((a) * (b))),(((a) * (b)) + ((b) * (a)))*] is complex Element of COMPLEX
([*(((a) * (b)) - ((a) * (b))),(((a) * (b)) + ((b) * (a)))*]) is complex real ext-real Element of REAL

(d) is complex real ext-real Element of REAL
([*(((a) * (b)) - ((a) * (b))),(((a) * (b)) + ((b) * (a)))*]) is complex real ext-real Element of REAL
(d) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
a * b is complex set
((a * b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL
((a * b)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
((a) * (b)) + ((b) * (a)) is complex real ext-real Element of REAL
[*(((a) * (b)) - ((a) * (b))),(((a) * (b)) + ((b) * (a)))*] is complex Element of COMPLEX
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
a + b is complex set
((a + b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL
((a + b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL
[*((a) + (b)),((a) + (b))*] is complex Element of COMPLEX

a * () is complex set
((a * ())) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * (()) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * (()) is complex real ext-real Element of REAL
((a) * (())) - ((a) * (())) is complex real ext-real Element of REAL

0 * (()) is complex real ext-real Element of REAL
((a) * 0) - (0 * (())) is complex real ext-real Element of REAL

a * () is complex set
((a * ())) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * (()) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * (()) is complex real ext-real Element of REAL
((a) * (())) + ((a) * (())) is complex real ext-real Element of REAL

[*a,b*] is complex Element of COMPLEX
b * () is complex set
a + (b * ()) is complex set
((a + (b * ()))) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
((b * ())) is complex real ext-real Element of REAL
(a) + ((b * ())) is complex real ext-real Element of REAL
0 + ((b * ())) is complex real ext-real Element of REAL
((a + (b * ()))) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
((b * ())) is complex real ext-real Element of REAL
(a) + ((b * ())) is complex real ext-real Element of REAL

a + b is complex set
(a) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL
((a) + (b)) * () is complex set
((a) + (b)) + (((a) + (b)) * ()) is complex set
[*((a) + (b)),((a) + (b))*] is complex Element of COMPLEX

a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
a + b is complex set
((a + b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL
((a + b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL
[*((a) + (b)),((a) + (b))*] is complex Element of COMPLEX

a * b is complex set
(a) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
((a) * (b)) + ((b) * (a)) is complex real ext-real Element of REAL
(((a) * (b)) + ((b) * (a))) * () is complex set
(((a) * (b)) - ((a) * (b))) + ((((a) * (b)) + ((b) * (a))) * ()) is complex set
[*(((a) * (b)) - ((a) * (b))),(((a) * (b)) + ((b) * (a)))*] is complex Element of COMPLEX

a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
a * b is complex set
((a * b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL
((a * b)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
((a) * (b)) + ((b) * (a)) is complex real ext-real Element of REAL
[*(((a) * (b)) - ((a) * (b))),(((a) * (b)) + ((b) * (a)))*] is complex Element of COMPLEX

a * () is complex set
((a * ())) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * (()) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * (()) is complex real ext-real Element of REAL
((a) * (())) - ((a) * (())) is complex real ext-real Element of REAL

0 * (()) is complex real ext-real Element of REAL
((a) * 0) - (0 * (())) is complex real ext-real Element of REAL

a * () is complex set
((a * ())) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * (()) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * (()) is complex real ext-real Element of REAL
((a) * (())) + ((a) * (())) is complex real ext-real Element of REAL

b * () is complex set
a + (b * ()) is complex set
((a + (b * ()))) is complex real ext-real Element of REAL
((a + (b * ()))) is complex real ext-real Element of REAL

d * () is complex set
c + (d * ()) is complex set
[*c,d*] is complex Element of COMPLEX
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) + ((a) * ()) is complex set
[*(a),(a)*] is complex Element of COMPLEX
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
(b) is complex real ext-real Element of REAL
a * b is complex set
((a * b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a * b)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
((a) * (b)) + ((b) * (a)) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
(b) is complex real ext-real Element of REAL
a * b is complex set
((a * b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
- ((a) * (b)) is complex real ext-real Element of REAL
((a * b)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
((a) * (b)) + ((b) * (a)) is complex real ext-real Element of REAL
a is complex set
a * a is complex set
((a * a)) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL

(a) * (a) is complex real ext-real set
(a) is complex real ext-real Element of REAL

(a) * (a) is complex real ext-real set
((a) ^2) - ((a) ^2) is complex real ext-real Element of REAL
((a * a)) is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real Element of REAL
2 * ((a) * (a)) is complex real ext-real Element of REAL
((a) * (a)) + ((a) * (a)) is complex real ext-real Element of REAL

- a is complex set
(a) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(- (a)) * () is complex set
(- (a)) + ((- (a)) * ()) is complex set
[*(- (a)),(- (a))*] is complex Element of COMPLEX
([*(- (a)),(- (a))*],a) is complex Element of COMPLEX
([*(- (a)),(- (a))*]) is complex real ext-real Element of REAL
([*(- (a)),(- (a))*]) + (a) is complex real ext-real Element of REAL
([*(- (a)),(- (a))*]) is complex real ext-real Element of REAL
([*(- (a)),(- (a))*]) + (a) is complex real ext-real Element of REAL
[*(([*(- (a)),(- (a))*]) + (a)),(([*(- (a)),(- (a))*]) + (a))*] is complex Element of COMPLEX
(- (a)) + (a) is complex real ext-real Element of REAL
[*((- (a)) + (a)),(([*(- (a)),(- (a))*]) + (a))*] is complex Element of COMPLEX
(- (a)) + (a) is complex real ext-real Element of REAL
[*0,((- (a)) + (a))*] is complex Element of COMPLEX

a is complex set
- a is complex set
((- a)) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
((- a)) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(- (a)) * () is complex set
(- (a)) + ((- (a)) * ()) is complex set
((),()) is complex Element of COMPLEX
(()) is complex Element of COMPLEX

a - b is complex set
(a) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) - (b) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) - (b) is complex real ext-real Element of REAL
((a) - (b)) * () is complex set
((a) - (b)) + (((a) - (b)) * ()) is complex set
(a) * () is complex set
(a) + ((a) * ()) is complex set
(b) is complex Element of COMPLEX
(a,(b)) is complex Element of COMPLEX
- (b) is complex real ext-real Element of REAL
- (b) is complex real ext-real Element of REAL
(- (b)) * () is complex set
(- (b)) + ((- (b)) * ()) is complex set
a + ((- (b)) + ((- (b)) * ())) is complex set

a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
a - b is complex set
((a - b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) - (b) is complex real ext-real Element of REAL
((a - b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) - (b) is complex real ext-real Element of REAL
((a) - (b)) * () is complex set
((a) - (b)) + (((a) - (b)) * ()) is complex set
((((a) - (b)) + (((a) - (b)) * ()))) is complex real ext-real Element of REAL
((((a) - (b)) + (((a) - (b)) * ()))) is complex real ext-real Element of REAL

a " is complex set
(a) is complex real ext-real Element of REAL

(a) * (a) is complex real ext-real set
(a) is complex real ext-real Element of REAL

(a) * (a) is complex real ext-real set
((a) ^2) + ((a) ^2) is complex real ext-real Element of REAL
(a) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(- (a)) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
((- (a)) / (((a) ^2) + ((a) ^2))) * () is complex set
((a) / (((a) ^2) + ((a) ^2))) + (((- (a)) / (((a) ^2) + ((a) ^2))) * ()) is complex set

(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
((a) * (b)) + ((b) * (a)) is complex real ext-real Element of REAL
(a) / 1 is complex real ext-real Element of REAL
((a) / 1) * ((- (a)) / (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
((a) / (((a) ^2) + ((a) ^2))) * (a) is complex real ext-real Element of REAL
(((a) / 1) * ((- (a)) / (((a) ^2) + ((a) ^2)))) + (((a) / (((a) ^2) + ((a) ^2))) * (a)) is complex real ext-real Element of REAL
(a) * (- (a)) is complex real ext-real Element of REAL
1 * (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
((a) * (- (a))) / (1 * (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(((a) / (((a) ^2) + ((a) ^2))) * (a)) / 1 is complex real ext-real Element of REAL
(((a) * (- (a))) / (1 * (((a) ^2) + ((a) ^2)))) + ((((a) / (((a) ^2) + ((a) ^2))) * (a)) / 1) is complex real ext-real Element of REAL
(a) / 1 is complex real ext-real Element of REAL
((a) / 1) * (a) is complex real ext-real Element of REAL
(((a) / 1) * (a)) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
(((a) * (- (a))) / (1 * (((a) ^2) + ((a) ^2)))) + ((((a) / 1) * (a)) / (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real Element of REAL
- ((a) * (a)) is complex real ext-real Element of REAL
(- ((a) * (a))) + ((a) * (a)) is complex real ext-real Element of REAL
((- ((a) * (a))) + ((a) * (a))) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) - ((a) * (b)) is complex real ext-real Element of REAL
((a) / 1) * ((a) / (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(a) * ((- (a)) / (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(((a) / 1) * ((a) / (((a) ^2) + ((a) ^2)))) - ((a) * ((- (a)) / (((a) ^2) + ((a) ^2)))) is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real Element of REAL
((a) * (a)) / (1 * (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
((a) / 1) * ((- (a)) / (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(((a) * (a)) / (1 * (((a) ^2) + ((a) ^2)))) - (((a) / 1) * ((- (a)) / (((a) ^2) + ((a) ^2)))) is complex real ext-real Element of REAL
((a) ^2) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
(a) * (- (a)) is complex real ext-real Element of REAL
((a) * (- (a))) / (1 * (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(((a) ^2) / (((a) ^2) + ((a) ^2))) - (((a) * (- (a))) / (1 * (((a) ^2) + ((a) ^2)))) is complex real ext-real Element of REAL
- ((a) ^2) is complex real ext-real Element of REAL
(- ((a) ^2)) / (1 * (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(((a) ^2) / (((a) ^2) + ((a) ^2))) - ((- ((a) ^2)) / (1 * (((a) ^2) + ((a) ^2)))) is complex real ext-real Element of REAL
((a) ^2) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
- (((a) ^2) / (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(((a) ^2) / (((a) ^2) + ((a) ^2))) - (- (((a) ^2) / (((a) ^2) + ((a) ^2)))) is complex real ext-real Element of REAL
((a) ^2) / (1 * (((a) ^2) + ((a) ^2))) is complex real ext-real Element of REAL
(((a) ^2) / (((a) ^2) + ((a) ^2))) + (((a) ^2) / (1 * (((a) ^2) + ((a) ^2)))) is complex real ext-real Element of REAL
(((a) ^2) + ((a) ^2)) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
(a,b) is complex Element of COMPLEX
[*(((a) * (b)) - ((a) * (b))),(((a) * (b)) + ((b) * (a)))*] is complex Element of COMPLEX

a is complex set
a " is complex set
((a ")) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL

(a) * (a) is complex real ext-real set
(a) is complex real ext-real Element of REAL

(a) * (a) is complex real ext-real set
((a) ^2) + ((a) ^2) is complex real ext-real Element of REAL
(a) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
((a ")) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(- (a)) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
((- (a)) / (((a) ^2) + ((a) ^2))) * () is complex set
((a) / (((a) ^2) + ((a) ^2))) + (((- (a)) / (((a) ^2) + ((a) ^2))) * ()) is complex set
(()) is complex Element of COMPLEX
(()) ^2 is complex real ext-real Element of REAL
(()) * (()) is complex real ext-real set
(()) ^2 is complex real ext-real Element of REAL
(()) * (()) is complex real ext-real set
((()) ^2) + ((()) ^2) is complex real ext-real Element of REAL
(()) / (((()) ^2) + ((()) ^2)) is complex real ext-real Element of REAL
- (()) is complex real ext-real Element of REAL
(- (())) / (((()) ^2) + ((()) ^2)) is complex real ext-real Element of REAL
((- (())) / (((()) ^2) + ((()) ^2))) * () is complex set
((()) / (((()) ^2) + ((()) ^2))) + (((- (())) / (((()) ^2) + ((()) ^2))) * ()) is complex set
(()) is complex Element of COMPLEX
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
a " is complex set
((a ")) is complex real ext-real Element of REAL

((a ")) is complex real ext-real Element of REAL

(a) * (a) is complex real ext-real set

(a) * (a) is complex real ext-real set
((a) ^2) + ((a) ^2) is complex real ext-real Element of REAL
(a) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
1 * (a) is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real Element of REAL
(1 * (a)) / ((a) * (a)) is complex real ext-real Element of REAL
1 / (a) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(- (a)) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
a " is complex set
((a ")) is complex real ext-real Element of REAL
((a ")) is complex real ext-real Element of REAL

- ((a) ") is complex real ext-real Element of REAL

(a) * (a) is complex real ext-real set

(a) * (a) is complex real ext-real set
((a) ^2) + ((a) ^2) is complex real ext-real Element of REAL
(a) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(- (a)) / (((a) ^2) + ((a) ^2)) is complex real ext-real Element of REAL
1 * (a) is complex real ext-real Element of REAL
(a) * (a) is complex real ext-real Element of REAL
(1 * (a)) / ((a) * (a)) is complex real ext-real Element of REAL
- ((1 * (a)) / ((a) * (a))) is complex real ext-real Element of REAL
1 / (a) is complex real ext-real Element of REAL
- (1 / (a)) is complex real ext-real Element of REAL
a is complex set
b is complex set
a / b is complex set
(a) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) + ((a) * (b)) is complex real ext-real Element of REAL

(b) * (b) is complex real ext-real set

(b) * (b) is complex real ext-real set
((b) ^2) + ((b) ^2) is complex real ext-real Element of REAL
(((a) * (b)) + ((a) * (b))) / (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((b) * (a)) - ((a) * (b)) is complex real ext-real Element of REAL
(((b) * (a)) - ((a) * (b))) / (((b) ^2) + ((b) ^2)) is complex real ext-real Element of REAL
((((b) * (a)) - ((a) * (b))) / (((b) ^2) + ((b) ^2))) * () is complex set
((((a) * (b)) + ((a) * (b))) / (((b) ^2) + ((b) ^2))) + (((((b) * (a)) - ((a) * (b))) / (((b) ^2) + ((b) ^2))) * ()) is complex set

(d) is complex real ext-real Element of REAL

(d) * (d) is complex real ext-real set
(d) is complex real ext-real Element of REAL

(d) * (d) is complex real ext-real set
((d) ^2) + ((d) ^2) is complex real ext-real Element of REAL
(d) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
- (d) is complex real ext-real Element of REAL
(- (d)) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
[*((d) / (((d) ^2) + ((d) ^2))),((- (d)) / (((d) ^2) + ((d) ^2)))*] is complex Element of COMPLEX
([*((d) / (((d) ^2) + ((d) ^2))),((- (d)) / (((d) ^2) + ((d) ^2)))*]) is complex real ext-real Element of REAL
((- (d)) / (((d) ^2) + ((d) ^2))) * () is complex set
((d) / (((d) ^2) + ((d) ^2))) + (((- (d)) / (((d) ^2) + ((d) ^2))) * ()) is complex set
((((d) / (((d) ^2) + ((d) ^2))) + (((- (d)) / (((d) ^2) + ((d) ^2))) * ()))) is complex real ext-real Element of REAL
([*((d) / (((d) ^2) + ((d) ^2))),((- (d)) / (((d) ^2) + ((d) ^2)))*]) is complex real ext-real Element of REAL
((((d) / (((d) ^2) + ((d) ^2))) + (((- (d)) / (((d) ^2) + ((d) ^2))) * ()))) is complex real ext-real Element of REAL

c / d is complex set
(d) is complex Element of COMPLEX
(c,(d)) is complex Element of COMPLEX
(c,[*((d) / (((d) ^2) + ((d) ^2))),((- (d)) / (((d) ^2) + ((d) ^2)))*]) is complex Element of COMPLEX
(c) is complex real ext-real Element of REAL
(c) / 1 is complex real ext-real Element of REAL
((c) / 1) * ((d) / (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
(c) is complex real ext-real Element of REAL
(c) * ((- (d)) / (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
(((c) / 1) * ((d) / (((d) ^2) + ((d) ^2)))) - ((c) * ((- (d)) / (((d) ^2) + ((d) ^2)))) is complex real ext-real Element of REAL
(c) * ((- (d)) / (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
((d) / (((d) ^2) + ((d) ^2))) * (c) is complex real ext-real Element of REAL
((c) * ((- (d)) / (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * (c)) is complex real ext-real Element of REAL
[*((((c) / 1) * ((d) / (((d) ^2) + ((d) ^2)))) - ((c) * ((- (d)) / (((d) ^2) + ((d) ^2))))),(((c) * ((- (d)) / (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * (c)))*] is complex Element of COMPLEX
(((c) * ((- (d)) / (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * (c))) * () is complex set
((((c) / 1) * ((d) / (((d) ^2) + ((d) ^2)))) - ((c) * ((- (d)) / (((d) ^2) + ((d) ^2))))) + ((((c) * ((- (d)) / (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * (c))) * ()) is complex set
(c) * (d) is complex real ext-real Element of REAL
1 * (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
((c) * (d)) / (1 * (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
(c) / 1 is complex real ext-real Element of REAL
((c) / 1) * ((- (d)) / (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
(((c) * (d)) / (1 * (((d) ^2) + ((d) ^2)))) - (((c) / 1) * ((- (d)) / (((d) ^2) + ((d) ^2)))) is complex real ext-real Element of REAL
((((c) * (d)) / (1 * (((d) ^2) + ((d) ^2)))) - (((c) / 1) * ((- (d)) / (((d) ^2) + ((d) ^2))))) + ((((c) * ((- (d)) / (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * (c))) * ()) is complex set
((c) * (d)) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
(c) * (- (d)) is complex real ext-real Element of REAL
((c) * (- (d))) / (1 * (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
(((c) * (d)) / (((d) ^2) + ((d) ^2))) - (((c) * (- (d))) / (1 * (((d) ^2) + ((d) ^2)))) is complex real ext-real Element of REAL
((c) / 1) * ((- (d)) / (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
(((c) / 1) * ((- (d)) / (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * (c)) is complex real ext-real Element of REAL
((((c) / 1) * ((- (d)) / (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * (c))) * () is complex set
((((c) * (d)) / (((d) ^2) + ((d) ^2))) - (((c) * (- (d))) / (1 * (((d) ^2) + ((d) ^2))))) + (((((c) / 1) * ((- (d)) / (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * (c))) * ()) is complex set
((c) * (- (d))) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
(((c) * (d)) / (((d) ^2) + ((d) ^2))) - (((c) * (- (d))) / (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
(c) * (- (d)) is complex real ext-real Element of REAL
((c) * (- (d))) / (1 * (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
((d) / (((d) ^2) + ((d) ^2))) * ((c) / 1) is complex real ext-real Element of REAL
(((c) * (- (d))) / (1 * (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * ((c) / 1)) is complex real ext-real Element of REAL
((((c) * (- (d))) / (1 * (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * ((c) / 1))) * () is complex set
((((c) * (d)) / (((d) ^2) + ((d) ^2))) - (((c) * (- (d))) / (((d) ^2) + ((d) ^2)))) + (((((c) * (- (d))) / (1 * (((d) ^2) + ((d) ^2)))) + (((d) / (((d) ^2) + ((d) ^2))) * ((c) / 1))) * ()) is complex set
((c) * (- (d))) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
(c) * (d) is complex real ext-real Element of REAL
((c) * (d)) / (1 * (((d) ^2) + ((d) ^2))) is complex real ext-real Element of REAL
(((c) * (- (d))) / (((d) ^2) + ((d) ^2))) + (((c) * (d)) / (1 * (((d) ^2) + ((d) ^2)))) is complex real ext-real Element of REAL
((((c) * (- (d))) / (((d) ^2) + ((d) ^2))) + (((c) * (d)) / (1 * (((d) ^2) + ((d) ^2))))) * () is complex set
((((c) * (d)) / (((d) ^2) + ((d) ^2))) - (((c) * (- (d))) / (((d) ^2) + ((d) ^2)))) + (((((c) * (- (d))) / (((d) ^2) + ((d) ^2))) + (((c) * (d)) / (1 * (((d) ^2) + ((d) ^2))))) * ()) is complex set
((c) * (d)) - ((c) * (- (d))) is complex real ext-real Element of REAL
(((c) * (d)) - ((c) * (- (d)))) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
((((c) * (d)) - ((c) * (- (d)))) / (((d) ^2) + ((d) ^2))) + (((((c) * (- (d))) / (((d) ^2) + ((d) ^2))) + (((c) * (d)) / (1 * (((d) ^2) + ((d) ^2))))) * ()) is complex set
(c) * (d) is complex real ext-real Element of REAL
((c) * (d)) + ((c) * (d)) is complex real ext-real Element of REAL
(((c) * (d)) + ((c) * (d))) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
(c) * (d) is complex real ext-real Element of REAL
- ((c) * (d)) is complex real ext-real Element of REAL
(- ((c) * (d))) + ((c) * (d)) is complex real ext-real Element of REAL
((- ((c) * (d))) + ((c) * (d))) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
(((- ((c) * (d))) + ((c) * (d))) / (((d) ^2) + ((d) ^2))) * () is complex set
((((c) * (d)) + ((c) * (d))) / (((d) ^2) + ((d) ^2))) + ((((- ((c) * (d))) + ((c) * (d))) / (((d) ^2) + ((d) ^2))) * ()) is complex set
(d) * (c) is complex real ext-real Element of REAL
((d) * (c)) - ((c) * (d)) is complex real ext-real Element of REAL
(((d) * (c)) - ((c) * (d))) / (((d) ^2) + ((d) ^2)) is complex real ext-real Element of REAL
((((d) * (c)) - ((c) * (d))) / (((d) ^2) + ((d) ^2))) * () is complex set
((((c) * (d)) + ((c) * (d))) / (((d) ^2) + ((d) ^2))) + (((((d) * (c)) - ((c) * (d))) / (((d) ^2) + ((d) ^2))) * ()) is complex set
i2 is complex Element of COMPLEX
y2 is complex Element of COMPLEX
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
(a,b) is complex Element of COMPLEX
((a,b)) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((a) * (b)) + ((a) * (b)) is complex real ext-real Element of REAL

(b) * (b) is complex real ext-real set

(b) * (b) is complex real ext-real set
((b) ^2) + ((b) ^2) is complex real ext-real Element of REAL
((((a) * (b)) + ((a) * (b))),(((b) ^2) + ((b) ^2))) is complex real ext-real Element of COMPLEX
((a,b)) is complex real ext-real Element of REAL
(b) * (a) is complex real ext-real Element of REAL
(a) * (b) is complex real ext-real Element of REAL
((b) * (a)) - ((a) * (b)) is complex real ext-real Element of REAL
((((b) * (a)) - ((a) * (b))),(((b) ^2) + ((b) ^2))) is complex real ext-real Element of COMPLEX
(((((b) * (a)) - ((a) * (b))),(((b) ^2) + ((b) ^2))),()) is complex Element of COMPLEX
(((((a) * (b)) + ((a) * (b))),(((b) ^2) + ((b) ^2))),(((((b) * (a)) - ((a) * (b))),(((b) ^2) + ((b) ^2))),())) is complex Element of COMPLEX
((((((a) * (b)) + ((a) * (b))),(((b) ^2) + ((b) ^2))),(((((b) * (a)) - ((a) * (b))),(((b) ^2) + ((b) ^2))),()))) is complex real ext-real Element of REAL
((((((a) * (b)) + ((a) * (b))),(((b) ^2) + ((b) ^2))),(((((b) * (a)) - ((a) * (b))),(((b) ^2) + ((b) ^2))),()))) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
(b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a,b) is complex Element of COMPLEX
((a,b)) is complex real ext-real Element of REAL
((a),(b)) is complex real ext-real Element of COMPLEX
((a,b)) is complex real ext-real Element of REAL
b " is complex set
a * (b ") is complex set
((b ")) is complex real ext-real Element of REAL
((b ")) is complex real ext-real Element of REAL
(a) * ((b ")) is complex real ext-real Element of REAL

(a) * ((b) ") is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
b is complex set
(b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(a,b) is complex Element of COMPLEX
((a,b)) is complex real ext-real Element of REAL
((a),(b)) is complex real ext-real Element of COMPLEX
((a,b)) is complex real ext-real Element of REAL
b " is complex set
a * (b ") is complex set
((b ")) is complex real ext-real Element of REAL
((b ")) is complex real ext-real Element of REAL
(a) * ((b ")) is complex real ext-real Element of REAL
- ((a) * ((b "))) is complex real ext-real Element of REAL

- ((b) ") is complex real ext-real Element of REAL
(a) * (- ((b) ")) is complex real ext-real Element of REAL
- ((a) * (- ((b) "))) is complex real ext-real Element of REAL
(a) * ((b) ") is complex real ext-real Element of REAL
- ((a) * ((b) ")) is complex real ext-real Element of REAL
- (- ((a) * ((b) "))) is complex real ext-real Element of REAL
a is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
b is complex set
c is complex set
(c) is complex real ext-real Element of REAL
(c) is complex real ext-real Element of REAL
(c) * () is complex set
(c) - ((c) * ()) is complex set
(b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(b) * () is complex set
(b) - ((b) * ()) is complex set
- (c) is complex real ext-real Element of REAL
(- (c)) * () is complex set
(c) + ((- (c)) * ()) is complex set
- (b) is complex real ext-real Element of REAL
- (- (c)) is complex real ext-real Element of REAL
(- (b)) * () is complex set
(b) + ((- (b)) * ()) is complex set
a is complex set
(a) is complex set
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
a is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
((a)) is complex real ext-real Element of REAL
((a)) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(- (a)) * () is complex set
(a) + ((- (a)) * ()) is complex set
(0) is complex Element of COMPLEX
(0) * () is complex set
(0) - ((0) * ()) is complex set
a is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
- (a) is complex real ext-real Element of REAL
(- (a)) * () is complex set
(a) + ((- (a)) * ()) is complex set
(()) is complex Element of COMPLEX
(()) * () is complex set
(()) - ((()) * ()) is complex set
(()) is complex Element of COMPLEX
(()) * () is complex set
(()) - ((()) * ()) is complex set
a is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
b is complex set
a + b is complex set
((a + b)) is complex Element of COMPLEX
((a + b)) is complex real ext-real Element of REAL
((a + b)) is complex real ext-real Element of REAL
((a + b)) * () is complex set
((a + b)) - (((a + b)) * ()) is complex set
(b) is complex Element of COMPLEX
(b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(b) * () is complex set
(b) - ((b) * ()) is complex set
((a),(b)) is complex Element of COMPLEX
(((a + b))) is complex real ext-real Element of REAL
(a) + (b) is complex real ext-real Element of REAL
((a)) is complex real ext-real Element of REAL
((a)) + (b) is complex real ext-real Element of REAL
((b)) is complex real ext-real Element of REAL
((a)) + ((b)) is complex real ext-real Element of REAL
(((a),(b))) is complex real ext-real Element of REAL
(((a + b))) is complex real ext-real Element of REAL
(((a),(b))) is complex real ext-real Element of REAL
- ((a + b)) is complex real ext-real Element of REAL
- (b) is complex real ext-real Element of REAL
- (- (b)) is complex real ext-real Element of REAL
(a) + (- (- (b))) is complex real ext-real Element of REAL
- ((a) + (- (- (b)))) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
(- (a)) + (- (b)) is complex real ext-real Element of REAL
((a)) is complex real ext-real Element of REAL
((a)) + (- (b)) is complex real ext-real Element of REAL
((b)) is complex real ext-real Element of REAL
((a)) + ((b)) is complex real ext-real Element of REAL
a is complex set
- a is complex set
((- a)) is complex Element of COMPLEX
((- a)) is complex real ext-real Element of REAL
((- a)) is complex real ext-real Element of REAL
((- a)) * () is complex set
((- a)) - (((- a)) * ()) is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
((a)) is complex Element of COMPLEX
(((- a))) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
((a)) is complex real ext-real Element of REAL
- ((a)) is complex real ext-real Element of REAL
(((a))) is complex real ext-real Element of REAL
(((- a))) is complex real ext-real Element of REAL
(((a))) is complex real ext-real Element of REAL
- ((- a)) is complex real ext-real Element of REAL
- (a) is complex real ext-real Element of REAL
- (- (a)) is complex real ext-real Element of REAL
((a)) is complex real ext-real Element of REAL
- ((a)) is complex real ext-real Element of REAL
a is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
b is complex set
a - b is complex set
((a - b)) is complex Element of COMPLEX
((a - b)) is complex real ext-real Element of REAL
((a - b)) is complex real ext-real Element of REAL
((a - b)) * () is complex set
((a - b)) - (((a - b)) * ()) is complex set
(b) is complex Element of COMPLEX
(b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(b) * () is complex set
(b) - ((b) * ()) is complex set
((a),(b)) is complex Element of COMPLEX
- b is complex set
a + (- b) is complex set
((a + (- b))) is complex Element of COMPLEX
((a + (- b))) is complex real ext-real Element of REAL
((a + (- b))) is complex real ext-real Element of REAL
((a + (- b))) * () is complex set
((a + (- b))) - (((a + (- b))) * ()) is complex set
((- b)) is complex Element of COMPLEX
((- b)) is complex real ext-real Element of REAL
((- b)) is complex real ext-real Element of REAL
((- b)) * () is complex set
((- b)) - (((- b)) * ()) is complex set
((a),((- b))) is complex Element of COMPLEX
((b)) is complex Element of COMPLEX
((a),((b))) is complex Element of COMPLEX
a is complex set
(a) is complex Element of COMPLEX
(a) is complex real ext-real Element of REAL
(a) is complex real ext-real Element of REAL
(a) * () is complex set
(a) - ((a) * ()) is complex set
b is complex set
a * b is complex set
((a * b)) is complex Element of COMPLEX
((a * b)) is complex real ext-real Element of REAL
((a * b)) is complex real ext-real Element of REAL
((a * b)) * () is complex set
((a * b)) - (((a * b)) * ()) is complex set
(b) is complex Element of COMPLEX
(b) is complex real ext-real Element of REAL
(b) is complex real ext-real Element of REAL
(b) * () is complex set
(b) - ((b) * ()) is complex set
((a),(b)) is complex Element of COMPLEX
((a)) is complex real ext-real Element of REAL
((b)) is complex real