:: COMPLEX2 semantic presentation

REAL is non zero V50() V61() V62() V63() V67() set

NAT is V61() V62() V63() V64() V65() V66() V67() Element of K19(REAL)

K19(REAL) is set

COMPLEX is non zero V50() V61() V67() set

RAT is non zero V50() V61() V62() V63() V64() V67() set

INT is non zero V50() V61() V62() V63() V64() V65() V67() set

K20(COMPLEX,COMPLEX) is V35() set

K19(K20(COMPLEX,COMPLEX)) is set

K20(K20(COMPLEX,COMPLEX),COMPLEX) is V35() set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set

K20(REAL,REAL) is V35() V36() V37() set

K19(K20(REAL,REAL)) is set

K20(K20(REAL,REAL),REAL) is V35() V36() V37() set

K19(K20(K20(REAL,REAL),REAL)) is set

K20(RAT,RAT) is RAT -valued V35() V36() V37() set

K19(K20(RAT,RAT)) is set

K20(K20(RAT,RAT),RAT) is RAT -valued V35() V36() V37() set

K19(K20(K20(RAT,RAT),RAT)) is set

K20(INT,INT) is RAT -valued INT -valued V35() V36() V37() set

K19(K20(INT,INT)) is set

K20(K20(INT,INT),INT) is RAT -valued INT -valued V35() V36() V37() set

K19(K20(K20(INT,INT),INT)) is set

K20(NAT,NAT) is RAT -valued INT -valued V35() V36() V37() V38() set

K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued V35() V36() V37() V38() set

K19(K20(K20(NAT,NAT),NAT)) is set

omega is V61() V62() V63() V64() V65() V66() V67() set

K19(omega) is set

K19(NAT) is set

K20(NAT,REAL) is V35() V36() V37() set

K19(K20(NAT,REAL)) is set

K20(NAT,COMPLEX) is V35() set

K19(K20(NAT,COMPLEX)) is set

0 is zero natural complex real ext-real non positive non negative integer V34() V61() V62() V63() V64() V65() V66() V67() Element of NAT

2 is non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() Element of NAT

K20(2,REAL) is V35() V36() V37() set

K19(K20(2,REAL)) is set

1 is non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() Element of NAT

1r is complex Element of COMPLEX

Re 0 is complex real ext-real Element of REAL

Im 0 is complex real ext-real Element of REAL

<i> is complex Element of COMPLEX

K88(REAL,0,1,0,1) is Relation-like {0,1} -defined REAL -valued V6() V18({0,1}, REAL ) V35() V36() V37() Element of K19(K20({0,1},REAL))

{0,1} is non zero V61() V62() V63() V64() V65() V66() set

K20({0,1},REAL) is V35() V36() V37() set

K19(K20({0,1},REAL)) is set

1r *' is complex Element of COMPLEX

|.0.| is complex real ext-real Element of REAL

sin is Relation-like REAL -defined REAL -valued V6() V18( REAL , REAL ) V35() V36() V37() Element of K19(K20(REAL,REAL))

cos is Relation-like REAL -defined REAL -valued V6() V18( REAL , REAL ) V35() V36() V37() Element of K19(K20(REAL,REAL))

K426(REAL,sin) is V61() V62() V63() Element of K19(REAL)

K426(REAL,cos) is V61() V62() V63() Element of K19(REAL)

cos . 0 is complex real ext-real Element of REAL

sin . 0 is complex real ext-real Element of REAL

cos 0 is complex real ext-real Element of REAL

sin 0 is complex real ext-real Element of REAL

PI is complex real ext-real Element of REAL

PI / 2 is complex real ext-real Element of REAL

2 " is non zero complex real ext-real positive non negative set

PI * (2 ") is complex real ext-real set

cos . (PI / 2) is complex real ext-real Element of REAL

sin . (PI / 2) is complex real ext-real Element of REAL

cos . PI is complex real ext-real Element of REAL

- 1 is non zero complex real ext-real non positive negative integer Element of REAL

sin . PI is complex real ext-real Element of REAL

PI + (PI / 2) is complex real ext-real Element of REAL

cos . (PI + (PI / 2)) is complex real ext-real Element of REAL

sin . (PI + (PI / 2)) is complex real ext-real Element of REAL

2 * PI is complex real ext-real Element of REAL

cos . (2 * PI) is complex real ext-real Element of REAL

sin . (2 * PI) is complex real ext-real Element of REAL

cos (PI / 2) is complex real ext-real Element of REAL

sin (PI / 2) is complex real ext-real Element of REAL

cos PI is complex real ext-real Element of REAL

sin PI is complex real ext-real Element of REAL

cos (PI + (PI / 2)) is complex real ext-real Element of REAL

sin (PI + (PI / 2)) is complex real ext-real Element of REAL

cos (2 * PI) is complex real ext-real Element of REAL

sin (2 * PI) is complex real ext-real Element of REAL

- (PI / 2) is complex real ext-real Element of REAL

3 is non zero natural complex real ext-real positive non negative integer V34() V61() V62() V63() V64() V65() V66() Element of NAT

3 / 2 is non zero complex real ext-real positive non negative Element of REAL

3 * (2 ") is non zero complex real ext-real positive non negative set

(3 / 2) * PI is complex real ext-real Element of REAL

].0,(PI / 2).[ is V61() V62() V63() Element of K19(REAL)

].(PI / 2),PI.[ is V61() V62() V63() Element of K19(REAL)

K34(REAL,REAL,sin,].0,(PI / 2).[) is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of K19(K20(REAL,REAL))

K34(REAL,REAL,sin,].(PI / 2),PI.[) is Relation-like REAL -defined REAL -valued V6() V35() V36() V37() Element of K19(K20(REAL,REAL))

b is complex real ext-real set

a is complex real ext-real set

a / b is complex real ext-real Element of COMPLEX

b " is complex real ext-real set

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

[\(a / b)/] is complex real ext-real integer set

- [\(a / b)/] is complex real ext-real integer set

b * (- [\(a / b)/]) is complex real ext-real set

(b * (- [\(a / b)/])) + a is complex real ext-real set

A is complex real ext-real set

[\(a / b)/] * b is complex real ext-real set

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

- a is complex real ext-real set

- ([\(a / b)/] * b) is complex real ext-real set

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

(a / b) - 1 is complex real ext-real Element of REAL

- 1 is non zero complex real ext-real non positive negative integer set

(a / b) + (- 1) is complex real ext-real set

- ((a / b) - 1) is complex real ext-real Element of REAL

- (a / b) is complex real ext-real Element of COMPLEX

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

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

(- [\(a / b)/]) * b is complex real ext-real set

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

(- ((a / b) * b)) + b is complex real ext-real set

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

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

a is complex real ext-real set

b is complex real ext-real set

c is complex real ext-real set

0 + a is complex real ext-real Element of REAL

c + a is complex real ext-real set

r is complex real ext-real integer set

a * r is complex real ext-real set

c + (a * r) is complex real ext-real set

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

c - a is complex real ext-real set

- a is complex real ext-real set

c + (- a) is complex real ext-real set

0 + 1 is non zero complex real ext-real positive non negative integer Element of REAL

a is complex real ext-real set

b is complex real ext-real set

a - b is complex real ext-real set

- b is complex real ext-real set

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

sin (a - b) is complex real ext-real set

sin a is complex real ext-real set

cos b is complex real ext-real set

(sin a) * (cos b) is complex real ext-real set

cos a is complex real ext-real set

sin b is complex real ext-real set

(cos a) * (sin b) is complex real ext-real set

((sin a) * (cos b)) - ((cos a) * (sin b)) is complex real ext-real set

- ((cos a) * (sin b)) is complex real ext-real set

((sin a) * (cos b)) + (- ((cos a) * (sin b))) is complex real ext-real set

cos (a - b) is complex real ext-real set

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

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

((cos a) * (cos b)) + ((sin a) * (sin b)) is complex real ext-real set

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

sin . a is complex real ext-real Element of REAL

cos . (- b) is complex real ext-real Element of REAL

(sin . a) * (cos . (- b)) is complex real ext-real Element of REAL

cos . a is complex real ext-real Element of REAL

sin . (- b) is complex real ext-real Element of REAL

(cos . a) * (sin . (- b)) is complex real ext-real Element of REAL

((sin . a) * (cos . (- b))) + ((cos . a) * (sin . (- b))) is complex real ext-real Element of REAL

cos . b is complex real ext-real Element of REAL

(sin . a) * (cos . b) is complex real ext-real Element of REAL

((sin . a) * (cos . b)) + ((cos . a) * (sin . (- b))) is complex real ext-real Element of REAL

sin . b is complex real ext-real Element of REAL

- (sin . b) is complex real ext-real Element of REAL

(cos . a) * (- (sin . b)) is complex real ext-real Element of REAL

((sin . a) * (cos . b)) + ((cos . a) * (- (sin . b))) is complex real ext-real Element of REAL

(sin a) * (cos . b) is complex real ext-real Element of REAL

(cos . a) * (sin . b) is complex real ext-real Element of REAL

((sin a) * (cos . b)) - ((cos . a) * (sin . b)) is complex real ext-real Element of REAL

- ((cos . a) * (sin . b)) is complex real ext-real set

((sin a) * (cos . b)) + (- ((cos . a) * (sin . b))) is complex real ext-real set

((sin a) * (cos b)) - ((cos . a) * (sin . b)) is complex real ext-real Element of REAL

((sin a) * (cos b)) + (- ((cos . a) * (sin . b))) is complex real ext-real set

(cos a) * (sin . b) is complex real ext-real Element of REAL

((sin a) * (cos b)) - ((cos a) * (sin . b)) is complex real ext-real Element of REAL

- ((cos a) * (sin . b)) is complex real ext-real set

((sin a) * (cos b)) + (- ((cos a) * (sin . b))) is complex real ext-real set

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

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

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

((cos . a) * (cos . (- b))) - ((sin . a) * (sin . (- b))) is complex real ext-real Element of REAL

- ((sin . a) * (sin . (- b))) is complex real ext-real set

((cos . a) * (cos . (- b))) + (- ((sin . a) * (sin . (- b)))) is complex real ext-real set

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

((cos . a) * (cos . b)) - ((sin . a) * (sin . (- b))) is complex real ext-real Element of REAL

((cos . a) * (cos . b)) + (- ((sin . a) * (sin . (- b)))) is complex real ext-real set

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

((cos . a) * (cos . b)) - ((sin . a) * (- (sin . b))) is complex real ext-real Element of REAL

- ((sin . a) * (- (sin . b))) is complex real ext-real set

((cos . a) * (cos . b)) + (- ((sin . a) * (- (sin . b)))) is complex real ext-real set

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

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

((cos a) * (cos . b)) + ((sin . a) * (sin . b)) is complex real ext-real Element of REAL

((cos a) * (cos b)) + ((sin . a) * (sin . b)) is complex real ext-real Element of REAL

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

((cos a) * (cos b)) + ((sin a) * (sin . b)) is complex real ext-real Element of REAL

a is complex real ext-real set

a - PI is complex real ext-real Element of REAL

- PI is complex real ext-real set

a + (- PI) is complex real ext-real set

sin . (a - PI) is complex real ext-real Element of REAL

sin . a is complex real ext-real Element of REAL

- (sin . a) is complex real ext-real Element of REAL

cos . (a - PI) is complex real ext-real Element of REAL

cos . a is complex real ext-real Element of REAL

- (cos . a) is complex real ext-real Element of REAL

- PI is complex real ext-real Element of REAL

cos . (- PI) is complex real ext-real Element of REAL

(sin . a) * (cos . (- PI)) is complex real ext-real Element of REAL

sin . (- PI) is complex real ext-real Element of REAL

(cos . a) * (sin . (- PI)) is complex real ext-real Element of REAL

((sin . a) * (cos . (- PI))) + ((cos . a) * (sin . (- PI))) is complex real ext-real Element of REAL

(sin . a) * (cos . PI) is complex real ext-real Element of REAL

((sin . a) * (cos . PI)) + ((cos . a) * (sin . (- PI))) is complex real ext-real Element of REAL

- (sin . PI) is complex real ext-real Element of REAL

(cos . a) * (- (sin . PI)) is complex real ext-real Element of REAL

((sin . a) * (cos . PI)) + ((cos . a) * (- (sin . PI))) is complex real ext-real Element of REAL

(cos . a) * (cos . (- PI)) is complex real ext-real Element of REAL

(sin . a) * (sin . (- PI)) is complex real ext-real Element of REAL

((cos . a) * (cos . (- PI))) - ((sin . a) * (sin . (- PI))) is complex real ext-real Element of REAL

- ((sin . a) * (sin . (- PI))) is complex real ext-real set

((cos . a) * (cos . (- PI))) + (- ((sin . a) * (sin . (- PI)))) is complex real ext-real set

(cos . a) * (cos . PI) is complex real ext-real Element of REAL

((cos . a) * (cos . PI)) - ((sin . a) * (sin . (- PI))) is complex real ext-real Element of REAL

((cos . a) * (cos . PI)) + (- ((sin . a) * (sin . (- PI)))) is complex real ext-real set

(sin . a) * (- (sin . PI)) is complex real ext-real Element of REAL

((cos . a) * (cos . PI)) - ((sin . a) * (- (sin . PI))) is complex real ext-real Element of REAL

- ((sin . a) * (- (sin . PI))) is complex real ext-real set

((cos . a) * (cos . PI)) + (- ((sin . a) * (- (sin . PI)))) is complex real ext-real set

a is complex real ext-real set

a - PI is complex real ext-real Element of REAL

- PI is complex real ext-real set

a + (- PI) is complex real ext-real set

sin (a - PI) is complex real ext-real Element of REAL

sin a is complex real ext-real set

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

cos (a - PI) is complex real ext-real Element of REAL

cos a is complex real ext-real set

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

(sin a) * (cos PI) is complex real ext-real Element of REAL

(cos a) * (sin PI) is complex real ext-real Element of REAL

((sin a) * (cos PI)) - ((cos a) * (sin PI)) is complex real ext-real Element of REAL

- ((cos a) * (sin PI)) is complex real ext-real set

((sin a) * (cos PI)) + (- ((cos a) * (sin PI))) is complex real ext-real set

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

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

((cos a) * (cos PI)) + ((sin a) * (sin PI)) is complex real ext-real Element of REAL

PI / 2 is complex real ext-real Element of COMPLEX

].0,(PI / 2).[ is V61() V62() V63() Element of K19(REAL)

a is complex real ext-real set

b is complex real ext-real set

sin b is complex real ext-real set

sin a is complex real ext-real set

dom sin is set

].0,(PI / 2).[ /\ (dom sin) is V61() V62() V63() Element of K19(REAL)

sin . a is complex real ext-real Element of REAL

sin . b is complex real ext-real Element of REAL

].(PI / 2),PI.[ is V61() V62() V63() Element of K19(REAL)

a is complex real ext-real set

b is complex real ext-real set

sin a is complex real ext-real set

sin b is complex real ext-real set

dom sin is set

].(PI / 2),PI.[ /\ (dom sin) is V61() V62() V63() Element of K19(REAL)

sin . a is complex real ext-real Element of REAL

sin . b is complex real ext-real Element of REAL

a is complex real ext-real set

sin a is complex real ext-real set

b is complex real ext-real integer set

(2 * PI) * b is complex real ext-real Element of REAL

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

sin (((2 * PI) * b) + a) is complex real ext-real Element of REAL

sin . a is complex real ext-real Element of REAL

sin . (((2 * PI) * b) + a) is complex real ext-real Element of REAL

- b is complex real ext-real integer set

(2 * PI) * (- b) is complex real ext-real Element of REAL

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

sin . (((2 * PI) * (- b)) + (((2 * PI) * b) + a)) is complex real ext-real Element of REAL

sin (((2 * PI) * (- b)) + (((2 * PI) * b) + a)) is complex real ext-real Element of REAL

c is natural complex real ext-real integer V34() V61() V62() V63() V64() V65() V66() Element of NAT

(2 * PI) * c is complex real ext-real Element of REAL

((2 * PI) * c) + a is complex real ext-real Element of REAL

sin (((2 * PI) * c) + a) is complex real ext-real Element of REAL

r is complex real ext-real Element of REAL

sin r is complex real ext-real Element of REAL

c is natural complex real ext-real integer V34() V61() V62() V63() V64() V65() V66() Element of NAT

(2 * PI) * c is complex real ext-real Element of REAL

((2 * PI) * c) + r is complex real ext-real Element of REAL

sin (((2 * PI) * c) + r) is complex real ext-real Element of REAL

a is complex real ext-real set

cos a is complex real ext-real set

b is complex real ext-real integer set

(2 * PI) * b is complex real ext-real Element of REAL

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

cos (((2 * PI) * b) + a) is complex real ext-real Element of REAL

cos . a is complex real ext-real Element of REAL

cos . (((2 * PI) * b) + a) is complex real ext-real Element of REAL

- b is complex real ext-real integer set

(2 * PI) * (- b) is complex real ext-real Element of REAL

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

cos . (((2 * PI) * (- b)) + (((2 * PI) * b) + a)) is complex real ext-real Element of REAL

cos (((2 * PI) * (- b)) + (((2 * PI) * b) + a)) is complex real ext-real Element of REAL

c is natural complex real ext-real integer V34() V61() V62() V63() V64() V65() V66() Element of NAT

(2 * PI) * c is complex real ext-real Element of REAL

((2 * PI) * c) + a is complex real ext-real Element of REAL

cos (((2 * PI) * c) + a) is complex real ext-real Element of REAL

r is complex real ext-real Element of REAL

cos r is complex real ext-real Element of REAL

c is natural complex real ext-real integer V34() V61() V62() V63() V64() V65() V66() Element of NAT

(2 * PI) * c is complex real ext-real Element of REAL

((2 * PI) * c) + r is complex real ext-real Element of REAL

cos (((2 * PI) * c) + r) is complex real ext-real Element of REAL

a is complex real ext-real set

sin a is complex real ext-real set

cos a is complex real ext-real set

a / (2 * PI) is complex real ext-real Element of COMPLEX

(2 * PI) " is complex real ext-real set

a * ((2 * PI) ") is complex real ext-real set

[\(a / (2 * PI))/] is complex real ext-real integer set

- [\(a / (2 * PI))/] is complex real ext-real integer set

(2 * PI) * (- [\(a / (2 * PI))/]) is complex real ext-real Element of REAL

((2 * PI) * (- [\(a / (2 * PI))/])) + a is complex real ext-real Element of REAL

b is complex real ext-real set

cos b is complex real ext-real set

sin b is complex real ext-real set

a is complex real ext-real set

b is complex real ext-real set

sin a is complex real ext-real set

sin b is complex real ext-real set

cos a is complex real ext-real set

cos b is complex real ext-real set

a - b is complex real ext-real set

- b is complex real ext-real set

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

cos (a - b) is complex real ext-real set

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

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

((cos a) * (cos b)) + ((sin a) * (sin b)) is complex real ext-real set

sin (a - b) is complex real ext-real set

(sin a) * (cos b) is complex real ext-real set

(cos a) * (sin b) is complex real ext-real set

((sin a) * (cos b)) - ((cos a) * (sin b)) is complex real ext-real set

- ((cos a) * (sin b)) is complex real ext-real set

((sin a) * (cos b)) + (- ((cos a) * (sin b))) is complex real ext-real set

b - a is complex real ext-real set

- a is complex real ext-real set

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

cos (b - a) is complex real ext-real set

sin (b - a) is complex real ext-real set

(sin b) * (cos a) is complex real ext-real set

(cos b) * (sin a) is complex real ext-real set

((sin b) * (cos a)) - ((cos b) * (sin a)) is complex real ext-real set

- ((cos b) * (sin a)) is complex real ext-real set

((sin b) * (cos a)) + (- ((cos b) * (sin a))) is complex real ext-real set

(2 * PI) + b is complex real ext-real Element of REAL

a + 0 is complex real ext-real Element of REAL

b + 0 is complex real ext-real Element of REAL

a + 0 is complex real ext-real Element of REAL

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

b + 0 is complex real ext-real Element of REAL

a is complex set

|.a.| is complex real ext-real Element of REAL

Arg a is complex real ext-real Element of REAL

cos (Arg a) is complex real ext-real Element of REAL

|.a.| * (cos (Arg a)) is complex real ext-real Element of REAL

sin (Arg a) is complex real ext-real Element of REAL

|.a.| * (sin (Arg a)) is complex real ext-real Element of REAL

(|.a.| * (sin (Arg a))) * <i> is complex set

(|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) is complex set

0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX

0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX

Arg 0 is complex real ext-real Element of REAL

a is complex set

Arg a is complex real ext-real Element of REAL

- a is complex set

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

(Arg a) + PI is complex real ext-real Element of REAL

(Arg a) - PI is complex real ext-real Element of REAL

- PI is complex real ext-real set

(Arg a) + (- PI) is complex real ext-real set

|.a.| is complex real ext-real Element of REAL

cos (Arg a) is complex real ext-real Element of REAL

|.a.| * (cos (Arg a)) is complex real ext-real Element of REAL

sin (Arg a) is complex real ext-real Element of REAL

|.a.| * (sin (Arg a)) is complex real ext-real Element of REAL

(|.a.| * (sin (Arg a))) * <i> is complex set

(|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) is complex set

- (|.a.| * (cos (Arg a))) is complex real ext-real Element of REAL

- (|.a.| * (sin (Arg a))) is complex real ext-real Element of REAL

(- (|.a.| * (sin (Arg a)))) * <i> is complex set

(- (|.a.| * (cos (Arg a)))) + ((- (|.a.| * (sin (Arg a)))) * <i>) is complex set

(2 * PI) + PI is complex real ext-real Element of REAL

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

|.(- a).| is complex real ext-real Element of REAL

cos (Arg (- a)) is complex real ext-real Element of REAL

|.(- a).| * (cos (Arg (- a))) is complex real ext-real Element of REAL

sin (Arg (- a)) is complex real ext-real Element of REAL

|.(- a).| * (sin (Arg (- a))) is complex real ext-real Element of REAL

(|.(- a).| * (sin (Arg (- a)))) * <i> is complex set

(|.(- a).| * (cos (Arg (- a)))) + ((|.(- a).| * (sin (Arg (- a)))) * <i>) is complex set

|.a.| * (sin (Arg (- a))) is complex real ext-real Element of REAL

- (sin (Arg a)) is complex real ext-real Element of REAL

|.a.| * (- (sin (Arg a))) is complex real ext-real Element of REAL

sin ((Arg a) + PI) is complex real ext-real Element of REAL

|.a.| * (cos (Arg (- a))) is complex real ext-real Element of REAL

- (cos (Arg a)) is complex real ext-real Element of REAL

|.a.| * (- (cos (Arg a))) is complex real ext-real Element of REAL

cos ((Arg a) + PI) is complex real ext-real Element of REAL

PI + PI is complex real ext-real Element of REAL

PI - PI is complex real ext-real Element of REAL

PI + (- PI) is complex real ext-real set

sin ((Arg a) - PI) is complex real ext-real Element of REAL

cos ((Arg a) - PI) is complex real ext-real Element of REAL

a is complex real ext-real Element of REAL

Arg a is complex real ext-real Element of REAL

|.a.| is complex real ext-real Element of REAL

0 * <i> is complex set

a + (0 * <i>) is complex set

cos (Arg a) is complex real ext-real Element of REAL

|.a.| * (cos (Arg a)) is complex real ext-real Element of REAL

sin (Arg a) is complex real ext-real Element of REAL

|.a.| * (sin (Arg a)) is complex real ext-real Element of REAL

(|.a.| * (sin (Arg a))) * <i> is complex set

(|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) is complex set

a is complex set

Arg a is complex real ext-real Element of REAL

|.a.| is complex real ext-real Element of REAL

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

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

(|.a.| * (sin 0)) * <i> is complex set

(|.a.| * (cos 0)) + ((|.a.| * (sin 0)) * <i>) is complex set

a is complex set

Arg a is complex real ext-real Element of REAL

- a is complex set

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

PI + 0 is complex real ext-real Element of REAL

PI + (Arg a) is complex real ext-real Element of REAL

PI + PI is complex real ext-real Element of REAL

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

- PI is complex real ext-real set

(PI + PI) + (- PI) is complex real ext-real set

(Arg (- a)) - PI is complex real ext-real Element of REAL

(Arg (- a)) + (- PI) is complex real ext-real set

- (- a) is complex set

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

a is complex set

b is complex set

a - b is complex set

- b is complex set

a + (- b) is complex set

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

b - a is complex set

- a is complex set

b + (- a) is complex set

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

0c is zero complex V61() V62() V63() V64() V65() V66() V67() Element of COMPLEX

- (a - b) is complex set

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

].0,PI.[ is V61() V62() V63() Element of K19(REAL)

a is complex set

Arg a is complex real ext-real Element of REAL

Im a is complex real ext-real Element of REAL

Re a is complex real ext-real Element of REAL

Re a is complex real ext-real Element of REAL

(Im a) * <i> is complex set

0 + ((Im a) * <i>) is complex set

Re a is complex real ext-real Element of REAL

Re a is complex real ext-real Element of REAL

Re a is complex real ext-real Element of REAL

a is complex set

Arg a is complex real ext-real Element of REAL

sin (Arg a) is complex real ext-real Element of REAL

Im a is complex real ext-real Element of REAL

Re a is complex real ext-real Element of REAL

Re a is complex real ext-real Element of REAL

(Im a) * <i> is complex set

0 + ((Im a) * <i>) is complex set

Re a is complex real ext-real Element of REAL

Re a is complex real ext-real Element of REAL

a is complex set

Arg a is complex real ext-real Element of REAL

b is complex set

Arg b is complex real ext-real Element of REAL

a + b is complex set

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

|.b.| is complex real ext-real Element of REAL

0 * <i> is complex set

|.b.| + (0 * <i>) is complex set

|.a.| is complex real ext-real Element of REAL

|.a.| + (0 * <i>) is complex set

Im a is complex real ext-real Element of REAL

|.a.| + |.b.| is complex real ext-real Element of REAL

(|.a.| + |.b.|) + (0 * <i>) is complex set

Im b is complex real ext-real Element of REAL

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

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

Im a is complex real ext-real Element of REAL

Im b is complex real ext-real Element of REAL

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

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

Im b is complex real ext-real Element of REAL

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

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

a is complex set

Arg a is complex real ext-real Element of REAL

Re a is complex real ext-real Element of REAL

Im a is complex real ext-real Element of REAL

|.a.| is complex real ext-real Element of REAL

0 * <i> is complex set

|.a.| + (0 * <i>) is complex set

(Re a) + (0 * <i>) is complex set

a is complex set

Arg a is complex real ext-real Element of REAL

Re a is complex real ext-real Element of REAL

Im a is complex real ext-real Element of REAL

|.a.| is complex real ext-real Element of REAL

|.a.| * (cos PI) is complex real ext-real Element of REAL

|.a.| * (sin PI) is complex real ext-real Element of REAL

(|.a.| * (sin PI)) * <i> is complex set

(|.a.| * (cos PI)) + ((|.a.| * (sin PI)) * <i>) is complex set

- |.a.| is complex real ext-real Element of REAL

- (- |.a.|) is complex real ext-real Element of REAL

0 * <i> is complex set

(Re a) + (0 * <i>) is complex set

a is complex set

Im a is complex real ext-real Element of REAL

Arg a is complex real ext-real Element of REAL

Re a is complex real ext-real Element of REAL

0 * <i> is complex set

(Re a) + (0 * <i>) is complex set

Arg ((Re a) + (0 * <i>)) is complex real ext-real Element of REAL

a is complex set

Arg a is complex real ext-real Element of REAL

Im a is complex real ext-real Element of REAL

a is complex Element of COMPLEX

- a is complex Element of COMPLEX

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

cos (Arg (- a)) is complex real ext-real Element of REAL

Arg a is complex real ext-real Element of REAL

cos (Arg a) is complex real ext-real Element of REAL

- (cos (Arg a)) is complex real ext-real Element of REAL

sin (Arg (- a)) is complex real ext-real Element of REAL

sin (Arg a) is complex real ext-real Element of REAL

- (sin (Arg 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.| * (cos (Arg a)) is complex real ext-real Element of REAL

|.a.| * (sin (Arg a)) is complex real ext-real Element of REAL

(|.a.| * (sin (Arg a))) * <i> is complex set

(|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) is complex set

|.(- a).| * (cos (Arg (- a))) is complex real ext-real Element of REAL

|.(- a).| * (sin (Arg (- a))) is complex real ext-real Element of REAL

(|.(- a).| * (sin (Arg (- a)))) * <i> is complex set

(|.(- a).| * (cos (Arg (- a)))) + ((|.(- a).| * (sin (Arg (- a)))) * <i>) is complex set

0 * <i> is complex set

0 + (0 * <i>) is complex set

|.a.| * (cos (Arg (- a))) is complex real ext-real Element of REAL

(|.a.| * (cos (Arg a))) + (|.a.| * (cos (Arg (- a)))) is complex real ext-real Element of REAL

|.a.| * (sin (Arg (- a))) is complex real ext-real Element of REAL

(|.a.| * (sin (Arg a))) + (|.a.| * (sin (Arg (- a)))) is complex real ext-real Element of REAL

((|.a.| * (sin (Arg a))) + (|.a.| * (sin (Arg (- a))))) * <i> is complex set

((|.a.| * (cos (Arg a))) + (|.a.| * (cos (Arg (- a))))) + (((|.a.| * (sin (Arg a))) + (|.a.| * (sin (Arg (- a))))) * <i>) is complex set

(sin (Arg a)) + (sin (Arg (- a))) is complex real ext-real Element of REAL

|.a.| * ((sin (Arg a)) + (sin (Arg (- a)))) is complex real ext-real Element of REAL

- (sin (Arg (- a))) is complex real ext-real Element of REAL

- (- (sin (Arg (- a)))) is complex real ext-real Element of REAL

(sin (Arg a)) + (- (- (sin (Arg (- a))))) is complex real ext-real Element of REAL

(cos (Arg a)) + (cos (Arg (- a))) is complex real ext-real Element of REAL

|.a.| * ((cos (Arg a)) + (cos (Arg (- a)))) is complex real ext-real Element of REAL

- (cos (Arg (- a))) is complex real ext-real Element of REAL

- (- (cos (Arg (- a)))) is complex real ext-real Element of REAL

(cos (Arg a)) + (- (- (cos (Arg (- a))))) is complex real ext-real Element of REAL

a is complex set

Arg a is complex real ext-real Element of REAL

cos (Arg a) is complex real ext-real Element of REAL

Re a is complex real ext-real Element of REAL

|.a.| is complex real ext-real Element of REAL

(Re a) / |.a.| is complex real ext-real Element of COMPLEX

|.a.| " is complex real ext-real set

(Re a) * (|.a.| ") is complex real ext-real set

sin (Arg a) is complex real ext-real Element of REAL

Im a is complex real ext-real Element of REAL

(Im a) / |.a.| is complex real ext-real Element of COMPLEX

(Im a) * (|.a.| ") is complex real ext-real set

|.a.| * (cos (Arg a)) is complex real ext-real Element of REAL

|.a.| * (sin (Arg a)) is complex real ext-real Element of REAL

(|.a.| * (sin (Arg a))) * <i> is complex set

(|.a.| * (cos (Arg a))) + ((|.a.| * (sin (Arg a))) * <i>) is complex set

a is complex set

Arg a is complex real ext-real Element of REAL

b is complex real ext-real Element of REAL

a * b is complex set

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

sin (Arg a) is complex real ext-real Element of REAL

Im a is complex real ext-real Element of REAL

|.a.| is complex real ext-real Element of REAL

(Im a) / |.a.| is complex real ext-real Element of COMPLEX

|.a.| " is complex real ext-real set

(Im a) * (|.a.| ") is complex real ext-real set

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

abs b is complex real ext-real Element of REAL

|.a.| * (abs b) is complex real ext-real Element of REAL

|.a.| * b is complex real ext-real Element of REAL

cos (Arg a) is complex real ext-real Element of REAL

Re a is complex real ext-real Element of REAL

(Re a) / |.a.| is complex real ext-real Element of COMPLEX

(Re a) * (|.a.| ") is complex real ext-real set

0 * <i> is complex set

b + (0 * <i>) is complex set

Re b is complex real ext-real Element of REAL

Im b is complex real ext-real Element of REAL

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

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

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

((Re a) * 0) + (b * (Im a)) is complex real ext-real Element of REAL

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

(Im (a * b)) / |.(a * b).| is complex real ext-real Element of COMPLEX

|.(a * b).| " is complex real ext-real set

(Im (a * b)) * (|.(a * b).| ") is complex real ext-real set

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

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

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

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

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

((Re a) * b) + (- (0 * (Im a))) is complex real ext-real set

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

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

(Re (a * b)) / |.(a * b).| is complex real ext-real Element of COMPLEX

(Re (a * b)) * (|.(a * b).| ") is complex real ext-real set

a is complex set

- a is complex set

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

b is complex real ext-real Element of REAL

a * b is complex set

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

Arg a is complex real ext-real Element of REAL

cos (Arg a) is complex real ext-real Element of REAL

Re a is complex real ext-real Element of REAL

|.a.| is complex real ext-real Element of REAL

(Re a) / |.a.| is complex real ext-real Element of COMPLEX

|.a.| " is complex real ext-real set

(Re a) * (|.a.| ") is complex real ext-real set

sin (Arg a) is complex real ext-real Element of REAL

Im a is complex real ext-real Element of REAL

(Im a) / |.a.| is complex real ext-real Element of COMPLEX

(Im a) * (|.a.| ") is complex real ext-real set

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

abs b is complex real ext-real Element of REAL

|.a.| * (abs 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

0 * <i> is complex set

b + (0 * <i>) is complex set

Re b is complex real ext-real Element of REAL

Im b is complex real ext-real Element of REAL

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

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

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

((Re a) * 0) + (b * (Im a)) is complex real ext-real Element of REAL

sin (Arg (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 * (Im a)) / (- (|.a.| * b)) is complex real ext-real Element of COMPLEX

(- (|.a.| * b)) " is complex real ext-real set

(b * (Im a)) * ((- (|.a.| * b)) ") is complex real ext-real set

(b * (Im a)) / (|.a.| * b) is complex real ext-real Element of COMPLEX

(|.a.| * b) " is complex real ext-real set

(b * (Im a)) * ((|.a.| * b) ") is complex real ext-real set

- ((b * (Im a)) / (|.a.| * b)) is complex real ext-real Element of COMPLEX

- (sin (Arg a)) is complex real ext-real Element of REAL

sin (Arg (- a)) is complex real ext-real Element of REAL

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

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

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

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

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

((Re a) * b) + (- (0 * (Im a))) is complex real ext-real set

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

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

(b * (Re a)) / (- (|.a.| * b)) is complex real ext-real Element of COMPLEX

(b * (Re a)) * ((- (|.a.| * b)) ") is complex real ext-real set

(b * (Re a)) / (|.a.| * b) is complex real ext-real Element of COMPLEX

(b * (Re a)) * ((|.a.| * b) ") is complex real ext-real set

- ((b * (Re a)) / (|.a.| * b)) is complex real ext-real Element of COMPLEX

- (cos (Arg a)) is complex real ext-real Element of REAL

cos (Arg (- a)) is complex real ext-real Element of REAL

a is complex set

b is complex set

b *' is complex Element of COMPLEX

a * (b *') is complex set

a is complex Element of COMPLEX

Re a is complex real ext-real Element of REAL

Im a is complex real ext-real Element of REAL

b is complex Element of COMPLEX

(a,b) is complex Element of COMPLEX

b *' is complex Element of COMPLEX

a * (b *') is complex set

Re b is complex real ext-real Element of REAL

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

Im b is complex real ext-real Element of REAL

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

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

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

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

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

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

((- ((Re a) * (Im b))) + ((Im a) * (Re b))) * <i> is complex set

(((Re a) * (Re b)) + ((Im a) * (Im b))) + (((- ((Re a) * (Im b))) + ((Im a) * (Re b))) * <i>) is complex set

(Im a) * <i> is complex set

(Re a) + ((Im a) * <i>) is complex set

(Im b) * <i> is complex set

(Re b) - ((Im b) * <i>) is complex set

- ((Im b) * <i>) is complex set

(Re b) + (- ((Im b) * <i>)) is complex set

a is complex Element of COMPLEX

(a,a) is complex Element of COMPLEX

a *' is complex Element of COMPLEX

a * (a *') is complex set

Re a is complex real ext-real Element of REAL

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

Im a is complex real ext-real Element of REAL

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

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

(Re a) ^2 is complex real ext-real Element of REAL

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

(Im a) ^2 is complex real ext-real Element of REAL

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

((Re a) ^2) + ((Im a) ^2) is complex real ext-real Element of REAL

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

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

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

((- ((Im a) * (Re a))) + ((Im a) * (Re a))) * <i> is complex set

(((Re a) * (Re a)) + ((Im a) * (Im a))) + (((- ((Im a) * (Re a))) + ((Im a) * (Re a))) * <i>) is complex set

a is complex Element of COMPLEX

(a,a) is complex Element of COMPLEX

a *' is complex Element of COMPLEX

a * (a *') is complex set

|.a.| is complex real ext-real Element of REAL

|.a.| ^2 is complex real ext-real Element of REAL

|.a.| * |.a.| is complex real ext-real set

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

Re a is complex real ext-real Element of REAL

(Re a) ^2 is complex real ext-real Element of REAL

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

Im a is complex real ext-real Element of REAL

(Im a) ^2 is complex real ext-real Element of REAL

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

((Re a) ^2) + ((Im a) ^2) is complex real ext-real Element of REAL

sqrt (((Re a) ^2) + ((Im a) ^2)) is complex real ext-real Element of REAL

0 * <i> is complex set

(|.a.| ^2) + (0 * <i>) is complex set

a is complex Element of COMPLEX

|.a.| is complex real ext-real Element of REAL

b is complex Element of COMPLEX

(a,b) is complex Element of COMPLEX

b *' is complex Element of COMPLEX

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 is complex Element of COMPLEX

(a,a) is complex Element of COMPLEX

a *' is complex Element of COMPLEX

a * (a *') is complex set

Re a is complex real ext-real Element of REAL

(Re a) ^2 is complex real ext-real Element of REAL

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

Im a is complex real ext-real Element of REAL

(Im a) ^2 is complex real ext-real Element of REAL

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

((Re a) ^2) + ((Im a) ^2) is complex real ext-real Element of REAL

a is complex Element of COMPLEX

b is complex Element of COMPLEX

(a,b) is complex Element of COMPLEX

b *' is complex Element of COMPLEX

a * (b *') is complex set

(b,a) is complex Element of COMPLEX

a *' is complex Element of COMPLEX

b * (a *') is complex set

(b,a) *' is complex Element of COMPLEX

a * (b *') is complex Element of COMPLEX

(a * (b *')) *' is complex Element of COMPLEX

((a * (b *')) *') *' is complex Element of COMPLEX

(b *') *' is complex Element of COMPLEX

((b *') *') * (a *') is complex Element of COMPLEX

(((b *') *') * (a *')) *' is complex Element of COMPLEX

a is complex Element of COMPLEX

b is complex Element of COMPLEX

a + b is complex Element of COMPLEX

c is complex Element of COMPLEX

((a + b),c) is complex Element of COMPLEX

c *' is complex Element of COMPLEX

(a + b) * (c *') is complex set

(a,c) is complex Element of COMPLEX

a * (c *') is complex set

(b,c) is complex Element of COMPLEX

b * (c *') is complex set

(a,c) + (b,c) is complex Element of COMPLEX

a is complex Element of COMPLEX

b is complex Element of COMPLEX

(a,b) is complex Element of COMPLEX

b *' is complex Element of COMPLEX

a * (b *') is complex set

c is complex Element of COMPLEX

b + c is complex Element of COMPLEX

(a,(b + c)) is complex Element of COMPLEX

(b + c) *' is complex Element of COMPLEX

a * ((b + c) *') is complex set

(a,c) is complex Element of COMPLEX

c *' is complex Element of COMPLEX

a * (c *') is complex set

(a,b) + (a,c) is complex Element of COMPLEX

(b *') + (c *') is complex Element of COMPLEX

a * ((b *') + (c *')) is complex Element of COMPLEX

a is complex Element of COMPLEX

b is complex Element of COMPLEX

a * b is complex Element of COMPLEX

c is complex Element of COMPLEX

((a * b),c) is complex Element of COMPLEX

c *' is complex Element of COMPLEX

(a * b) * (c *') is complex set

(b,c) is complex Element of COMPLEX

b * (c *') is complex set

a * (b,c) is complex Element of COMPLEX

a is complex Element of COMPLEX

b is complex Element of COMPLEX

b *' is complex Element of COMPLEX

c is complex Element of COMPLEX

b * c is complex Element of COMPLEX

(a,(b * c)) is complex Element of COMPLEX

(b * c) *' is complex Element of COMPLEX

a * ((b * c) *') is complex set

(a,c) is complex Element of COMPLEX

c *' is complex Element of COMPLEX

a * (c *') is complex set

(b *') * (a,c) is complex Element of COMPLEX

(b *') * (c *') is complex Element of COMPLEX

a * ((b *') * (c *')) is complex Element of COMPLEX

a is complex Element of COMPLEX

a *' is complex Element of COMPLEX

b is complex Element of COMPLEX

a * b is complex Element of COMPLEX

c is complex Element of COMPLEX

((a * b),c) is complex Element of COMPLEX

c *' is complex Element of COMPLEX

(a * b) * (c *') is complex set

(a *') * c is complex Element of COMPLEX

(b,((a *') * c)) is complex Element of COMPLEX

((a *') * c) *' is complex Element of COMPLEX

b * (((a *') * c) *') is complex set

(a *') *' is complex Element of COMPLEX

((a *') *') * (c *') is complex Element of COMPLEX

b * (((a *') *') * (c *')) is complex Element of COMPLEX

a is complex Element of COMPLEX

b is complex Element of COMPLEX

a * b is complex Element of COMPLEX

c is complex Element of COMPLEX

r is complex Element of COMPLEX

c * r is complex Element of COMPLEX

(a * b) + (c * r) is complex Element of COMPLEX

A is complex Element of COMPLEX

(((a * b) + (c * r)),A) is complex Element of COMPLEX

A *' is complex Element of COMPLEX

((a * b) + (c * r)) * (A *') is complex set

(b,A) is complex Element of COMPLEX

b * (A *') is complex set

a * (b,A) is complex Element of COMPLEX

(r,A) is complex Element of COMPLEX

r * (A *') is complex set

c * (r,A) is complex Element of COMPLEX

(a * (b,A)) + (c * (r,A)) is complex Element of COMPLEX

a is complex Element of COMPLEX

b is complex Element of COMPLEX

b *' is complex Element of COMPLEX

c is complex Element of COMPLEX

b * c is complex Element of COMPLEX

(a,c) is complex Element of COMPLEX

c *' is complex Element of COMPLEX

a * (c *') is complex set

(b *') * (a,c) is complex Element of COMPLEX

r is complex Element of COMPLEX

r *' is complex Element of COMPLEX

A is complex Element of COMPLEX

r * A is complex Element of COMPLEX

(b * c) + (r * A) is complex Element of COMPLEX

(a,((b * c) + (r * A))) is complex Element of COMPLEX

((b * c) + (r * A)) *' is complex Element of COMPLEX

a * (((b * c) + (r * A)) *') is complex set

(a,A) is complex Element of COMPLEX

A *' is complex Element of COMPLEX

a * (A *') is complex set

(r *') * (a,A) is complex Element of COMPLEX

((b *') * (a,c)) + ((r *') * (a,A)) is complex Element of COMPLEX

(a,(b * c)) is complex Element of COMPLEX

(b * c) *' is complex Element of COMPLEX

a * ((b * c) *') is complex set

(a,(r * A)) is complex Element of COMPLEX

(r * A) *' is complex Element of COMPLEX

a * ((r * A) *') is complex set

(a,(b * c)) + (a,(r * A)) is complex Element of COMPLEX

((b *') * (a,c)) + (a,(r * A)) is complex Element of COMPLEX

a is complex Element of COMPLEX

- a is complex Element of COMPLEX

b is complex Element of COMPLEX

((- a),b) is complex Element of COMPLEX

b *' is complex Element of COMPLEX

(- a) * (b *') is complex set

- b is complex Element of COMPLEX

(a,(- b)) is complex Element of COMPLEX

(- b) *' is complex Element of COMPLEX

a * ((- b) *') is complex set

- (1r *') is complex Element of COMPLEX

(a,b) is complex Element of COMPLEX

a * (b *') is complex set

(- (1r *')) * (a,b) is complex Element of COMPLEX

- 1r is complex Element of COMPLEX

(- 1r) *' is complex Element of COMPLEX

((- 1r) *') * (a,b) is complex Element of COMPLEX

(- 1r) * b is complex Element of COMPLEX

(a,((- 1r) * b)) is complex Element of COMPLEX

((- 1r) * b) *' is complex Element of COMPLEX

a * (((- 1r) * b) *') is complex set

a is complex Element of COMPLEX

- a is complex Element of COMPLEX

b is complex Element of COMPLEX

((- a),b) is complex Element of COMPLEX

b *' is complex Element of COMPLEX

(- a) * (b *') is complex set

(a,b) is complex Element of COMPLEX

a * (b *') is complex set

- (a,b) is complex Element of COMPLEX

a is complex Element of COMPLEX

b is complex Element of COMPLEX

(a,b) is complex Element of COMPLEX

b *' is complex Element of COMPLEX

a * (b *') is complex set

- (a,b) is complex Element of COMPLEX

- b is complex Element of COMPLEX

(a,(- b)) is complex Element of COMPLEX

(- b) *' is complex Element of COMPLEX

a * ((- b) *') is complex set

- a is complex Element of COMPLEX

((- a),b) is complex Element of COMPLEX

(- a) * (b *') is complex set

a is complex Element of COMPLEX

- a is complex Element of COMPLEX

b is complex Element of COMPLEX

- b is complex Element of COMPLEX

((- a),(- b)) is complex Element of COMPLEX

(- b) *' is complex Element of COMPLEX

(- a) * ((- b) *') is complex set

(a,b) is complex Element of COMPLEX

b *' is complex Element of COMPLEX

a * (b *') is