:: CFUNCDOM semantic presentation

REAL is non empty V37() set

COMPLEX is non empty V37() set
RAT is non empty V37() set
INT is non empty V37() set

NAT is set

1 is non empty set

1r is V21() Element of COMPLEX

c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] is set
[:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
C is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]

[x,y] is set
C . [x,y] is set

C is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
x is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]

[y,a] is set
C . [y,a] is set

x . [y,a] is set
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] is set
[:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
C is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]

[x,y] is set
C . [x,y] is set

C is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
x is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]

[y,a] is set
C . [y,a] is set

x . [y,a] is set
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
[:COMPLEX,(Funcs (c1,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
C is Relation-like [:COMPLEX,(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
x is V21() Element of COMPLEX

[x,y] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]

a is Element of c1
(C . [x,y]) . a is V21() Element of COMPLEX
y . a is V21() Element of COMPLEX
x * (y . a) is V21() Element of COMPLEX
C . (x,y) is Element of Funcs (c1,COMPLEX)
[x,y] is set
C . [x,y] is set

multcomplex . (x,(y . a)) is V21() Element of COMPLEX
[x,(y . a)] is set
multcomplex . [x,(y . a)] is set
C is Relation-like [:COMPLEX,(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
x is Relation-like [:COMPLEX,(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
y is V21() Element of COMPLEX

[y,a] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]

c6 is Element of c1
(C . [y,a]) . c6 is V21() Element of COMPLEX
a . c6 is V21() Element of COMPLEX
y * (a . c6) is V21() Element of COMPLEX

(x . [y,a]) . c6 is V21() Element of COMPLEX
C . (y,a) is Element of Funcs (c1,COMPLEX)
[y,a] is set
C . [y,a] is set
x . (y,a) is Element of Funcs (c1,COMPLEX)
x . [y,a] is set
c1 is non empty set
0 is empty Element of NAT

[:c1,REAL:] is set
bool [:c1,REAL:] is set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
0c is empty V21() Element of COMPLEX

[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
c1 is non empty set

[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
c1 is non empty set
C is non empty set
[:c1,C:] is set
bool [:c1,C:] is set
x is Element of c1

dom y is set
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] is set
[:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set

(c1) . (x,y) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[x,y] is set
(c1) . [x,y] is set
a is Element of c1

dom (addcomplex .: (x,y)) is set
((c1) . (x,y)) . a is V21() Element of COMPLEX
(addcomplex .: (x,y)) . a is V21() Element of COMPLEX
x . a is V21() Element of COMPLEX
y . a is V21() Element of COMPLEX
addcomplex . ((x . a),(y . a)) is V21() Element of COMPLEX
[(x . a),(y . a)] is set
addcomplex . [(x . a),(y . a)] is set
(x . a) + (y . a) is V21() Element of COMPLEX
C . a is V21() Element of COMPLEX
a is Element of c1
C . a is V21() Element of COMPLEX
(addcomplex .: (x,y)) . a is V21() Element of COMPLEX
x . a is V21() Element of COMPLEX
y . a is V21() Element of COMPLEX
addcomplex . ((x . a),(y . a)) is V21() Element of COMPLEX
[(x . a),(y . a)] is set
addcomplex . [(x . a),(y . a)] is set
(x . a) + (y . a) is V21() Element of COMPLEX
a is Element of c1
C . a is V21() Element of COMPLEX
x . a is V21() Element of COMPLEX
y . a is V21() Element of COMPLEX
(x . a) + (y . a) is V21() Element of COMPLEX
c6 is Element of c1
C . c6 is V21() Element of COMPLEX
x . c6 is V21() Element of COMPLEX
y . c6 is V21() Element of COMPLEX
(x . c6) + (y . c6) is V21() Element of COMPLEX
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] is set
[:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set

(c1) . (x,y) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[x,y] is set
(c1) . [x,y] is set
a is Element of c1

dom (multcomplex .: (x,y)) is set
((c1) . (x,y)) . a is V21() Element of COMPLEX
(multcomplex .: (x,y)) . a is V21() Element of COMPLEX
x . a is V21() Element of COMPLEX
y . a is V21() Element of COMPLEX
multcomplex . ((x . a),(y . a)) is V21() Element of COMPLEX
[(x . a),(y . a)] is set
multcomplex . [(x . a),(y . a)] is set
(x . a) * (y . a) is V21() Element of COMPLEX
C . a is V21() Element of COMPLEX
a is Element of c1
C . a is V21() Element of COMPLEX
(multcomplex .: (x,y)) . a is V21() Element of COMPLEX
x . a is V21() Element of COMPLEX
y . a is V21() Element of COMPLEX
multcomplex . ((x . a),(y . a)) is V21() Element of COMPLEX
[(x . a),(y . a)] is set
multcomplex . [(x . a),(y . a)] is set
(x . a) * (y . a) is V21() Element of COMPLEX
a is Element of c1
C . a is V21() Element of COMPLEX
x . a is V21() Element of COMPLEX
y . a is V21() Element of COMPLEX
(x . a) * (y . a) is V21() Element of COMPLEX
c6 is Element of c1
C . c6 is V21() Element of COMPLEX
x . c6 is V21() Element of COMPLEX
y . c6 is V21() Element of COMPLEX
(x . c6) * (y . c6) is V21() Element of COMPLEX
c1 is non empty set

Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX

[:c1,REAL:] is set
bool [:c1,REAL:] is set

[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
the Element of c1 is Element of c1
(c1) . the Element of c1 is V21() Element of COMPLEX
0c is empty V21() Element of COMPLEX
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like [:COMPLEX,(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:COMPLEX,(Funcs (c1,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set

y is V21() Element of COMPLEX
[y,x] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]

a is Element of c1
C . a is V21() Element of COMPLEX
x . a is V21() Element of COMPLEX
y * (x . a) is V21() Element of COMPLEX
a is Element of c1
C . a is V21() Element of COMPLEX
((c1) . [y,x]) . a is V21() Element of COMPLEX
x . a is V21() Element of COMPLEX
y * (x . a) is V21() Element of COMPLEX
a is Element of c1
C . a is V21() Element of COMPLEX
x . a is V21() Element of COMPLEX
y * (x . a) is V21() Element of COMPLEX
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] is set
[:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set

(c1) . (C,x) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[C,x] is set
(c1) . [C,x] is set
(c1) . (x,C) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[x,C] is set
(c1) . [x,C] is set
y is Element of c1
((c1) . (C,x)) . y is V21() Element of COMPLEX
x . y is V21() Element of COMPLEX
C . y is V21() Element of COMPLEX
(x . y) + (C . y) is V21() Element of COMPLEX
((c1) . (x,C)) . y is V21() Element of COMPLEX
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] is set
[:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set

(c1) . (C,x) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[C,x] is set
(c1) . [C,x] is set

(c1) . (x,y) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[x,y] is set
(c1) . [x,y] is set
(c1) . (C,((c1) . (x,y))) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[C,((c1) . (x,y))] is set
(c1) . [C,((c1) . (x,y))] is set
(c1) . (((c1) . (C,x)),y) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[((c1) . (C,x)),y] is set
(c1) . [((c1) . (C,x)),y] is set
a is Element of c1
((c1) . (C,((c1) . (x,y)))) . a is V21() Element of COMPLEX
C . a is V21() Element of COMPLEX
((c1) . (x,y)) . a is V21() Element of COMPLEX
(C . a) + (((c1) . (x,y)) . a) is V21() Element of COMPLEX
x . a is V21() Element of COMPLEX
y . a is V21() Element of COMPLEX
(x . a) + (y . a) is V21() Element of COMPLEX
(C . a) + ((x . a) + (y . a)) is V21() Element of COMPLEX
(C . a) + (x . a) is V21() Element of COMPLEX
((C . a) + (x . a)) + (y . a) is V21() Element of COMPLEX
((c1) . (C,x)) . a is V21() Element of COMPLEX
(((c1) . (C,x)) . a) + (y . a) is V21() Element of COMPLEX
((c1) . (((c1) . (C,x)),y)) . a is V21() Element of COMPLEX
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] is set
[:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set

(c1) . (C,x) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[C,x] is set
(c1) . [C,x] is set
(c1) . (x,C) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[x,C] is set
(c1) . [x,C] is set
y is Element of c1
((c1) . (C,x)) . y is V21() Element of COMPLEX
x . y is V21() Element of COMPLEX
C . y is V21() Element of COMPLEX
(x . y) * (C . y) is V21() Element of COMPLEX
((c1) . (x,C)) . y is V21() Element of COMPLEX
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] is set
[:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set

(c1) . (C,x) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[C,x] is set
(c1) . [C,x] is set

(c1) . (x,y) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[x,y] is set
(c1) . [x,y] is set
(c1) . (C,((c1) . (x,y))) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[C,((c1) . (x,y))] is set
(c1) . [C,((c1) . (x,y))] is set
(c1) . (((c1) . (C,x)),y) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[((c1) . (C,x)),y] is set
(c1) . [((c1) . (C,x)),y] is set
a is Element of c1
((c1) . (C,((c1) . (x,y)))) . a is V21() Element of COMPLEX
C . a is V21() Element of COMPLEX
((c1) . (x,y)) . a is V21() Element of COMPLEX
(C . a) * (((c1) . (x,y)) . a) is V21() Element of COMPLEX
x . a is V21() Element of COMPLEX
y . a is V21() Element of COMPLEX
(x . a) * (y . a) is V21() Element of COMPLEX
(C . a) * ((x . a) * (y . a)) is V21() Element of COMPLEX
(C . a) * (x . a) is V21() Element of COMPLEX
((C . a) * (x . a)) * (y . a) is V21() Element of COMPLEX
((c1) . (C,x)) . a is V21() Element of COMPLEX
(((c1) . (C,x)) . a) * (y . a) is V21() Element of COMPLEX
((c1) . (((c1) . (C,x)),y)) . a is V21() Element of COMPLEX
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] is set
[:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set

[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set

(c1) . ((c1),C) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[(c1),C] is set
(c1) . [(c1),C] is set
x is Element of c1
((c1) . ((c1),C)) . x is V21() Element of COMPLEX
(c1) . x is V21() Element of COMPLEX
C . x is V21() Element of COMPLEX
((c1) . x) * (C . x) is V21() Element of COMPLEX
1r * (C . x) is V21() Element of COMPLEX
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] is set
[:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set

[:c1,REAL:] is set
bool [:c1,REAL:] is set

(c1) . ((c1),C) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[(c1),C] is set
(c1) . [(c1),C] is set
x is Element of c1
((c1) . ((c1),C)) . x is V21() Element of COMPLEX
(c1) . x is V21() Element of COMPLEX
C . x is V21() Element of COMPLEX
((c1) . x) + (C . x) is V21() Element of COMPLEX
0c is empty V21() Element of COMPLEX
0c + (C . x) is V21() Element of COMPLEX
- 1r is V21() Element of COMPLEX
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] is set
[:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
(c1) is Relation-like [:COMPLEX,(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:COMPLEX,(Funcs (c1,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set

[:c1,REAL:] is set
bool [:c1,REAL:] is set

[(),C] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]

(c1) . (C,((c1) . [(),C])) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[C,((c1) . [(),C])] is set
(c1) . [C,((c1) . [(),C])] is set
x is Element of c1
C . x is V21() Element of COMPLEX
((c1) . (C,((c1) . [(),C]))) . x is V21() Element of COMPLEX
((c1) . [(),C]) . x is V21() Element of COMPLEX
(C . x) + (((c1) . [(),C]) . x) is V21() Element of COMPLEX
() * (C . x) is V21() Element of COMPLEX
(C . x) + (() * (C . x)) is V21() Element of COMPLEX
(c1) . x is V21() Element of COMPLEX
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like [:COMPLEX,(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:COMPLEX,(Funcs (c1,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set

[1r,C] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]

x is Element of c1
((c1) . [1r,C]) . x is V21() Element of COMPLEX
C . x is V21() Element of COMPLEX
1r * (C . x) is V21() Element of COMPLEX
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like [:COMPLEX,(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:COMPLEX,(Funcs (c1,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set

x is V21() set
y is V21() set
[y,C] is set
(c1) . [y,C] is set
[x,((c1) . [y,C])] is set
(c1) . [x,((c1) . [y,C])] is set
x * y is V21() Element of COMPLEX
[(x * y),C] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [(x * y),C] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
a is V21() Element of COMPLEX
c6 is V21() Element of COMPLEX
[c6,C] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]

[a,((c1) . [c6,C])] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [a,((c1) . [c6,C])] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
IT is Element of c1
((c1) . [a,((c1) . [c6,C])]) . IT is V21() Element of COMPLEX
((c1) . [c6,C]) . IT is V21() Element of COMPLEX
a * (((c1) . [c6,C]) . IT) is V21() Element of COMPLEX
C . IT is V21() Element of COMPLEX
c6 * (C . IT) is V21() Element of COMPLEX
a * (c6 * (C . IT)) is V21() Element of COMPLEX
a * c6 is V21() Element of COMPLEX
(a * c6) * (C . IT) is V21() Element of COMPLEX
[(a * c6),C] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [(a * c6),C] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
((c1) . [(a * c6),C]) . IT is V21() Element of COMPLEX
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] is set
[:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
(c1) is Relation-like [:COMPLEX,(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:COMPLEX,(Funcs (c1,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set

x is V21() set
[x,C] is set
(c1) . [x,C] is set
y is V21() set
[y,C] is set
(c1) . [y,C] is set
(c1) . (((c1) . [x,C]),((c1) . [y,C])) is set
[((c1) . [x,C]),((c1) . [y,C])] is set
(c1) . [((c1) . [x,C]),((c1) . [y,C])] is set
x + y is V21() Element of COMPLEX
[(x + y),C] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [(x + y),C] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
a is V21() Element of COMPLEX
[a,C] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]

c6 is V21() Element of COMPLEX
[c6,C] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]

(c1) . (((c1) . [a,C]),((c1) . [c6,C])) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[((c1) . [a,C]),((c1) . [c6,C])] is set
(c1) . [((c1) . [a,C]),((c1) . [c6,C])] is set
IT is Element of c1
((c1) . (((c1) . [a,C]),((c1) . [c6,C]))) . IT is V21() Element of COMPLEX
((c1) . [a,C]) . IT is V21() Element of COMPLEX
((c1) . [c6,C]) . IT is V21() Element of COMPLEX
(((c1) . [a,C]) . IT) + (((c1) . [c6,C]) . IT) is V21() Element of COMPLEX
C . IT is V21() Element of COMPLEX
a * (C . IT) is V21() Element of COMPLEX
(a * (C . IT)) + (((c1) . [c6,C]) . IT) is V21() Element of COMPLEX
c6 * (C . IT) is V21() Element of COMPLEX
(a * (C . IT)) + (c6 * (C . IT)) is V21() Element of COMPLEX
a + c6 is V21() Element of COMPLEX
(a + c6) * (C . IT) is V21() Element of COMPLEX
[(a + c6),C] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [(a + c6),C] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
((c1) . [(a + c6),C]) . IT is V21() Element of COMPLEX
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] is set
[:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
(c1) is Relation-like [:COMPLEX,(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:COMPLEX,(Funcs (c1,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set

(c1) . (C,x) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[C,x] is set
(c1) . [C,x] is set
y is V21() set
[y,C] is set
(c1) . [y,C] is set
[y,x] is set
(c1) . [y,x] is set
(c1) . (((c1) . [y,C]),((c1) . [y,x])) is set
[((c1) . [y,C]),((c1) . [y,x])] is set
(c1) . [((c1) . [y,C]),((c1) . [y,x])] is set
[y,((c1) . (C,x))] is set
(c1) . [y,((c1) . (C,x))] is set
a is V21() Element of COMPLEX
[a,C] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]

[a,x] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]

(c1) . (((c1) . [a,C]),((c1) . [a,x])) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[((c1) . [a,C]),((c1) . [a,x])] is set
(c1) . [((c1) . [a,C]),((c1) . [a,x])] is set
c6 is Element of c1
((c1) . (((c1) . [a,C]),((c1) . [a,x]))) . c6 is V21() Element of COMPLEX
((c1) . [a,C]) . c6 is V21() Element of COMPLEX
((c1) . [a,x]) . c6 is V21() Element of COMPLEX
(((c1) . [a,C]) . c6) + (((c1) . [a,x]) . c6) is V21() Element of COMPLEX
C . c6 is V21() Element of COMPLEX
a * (C . c6) is V21() Element of COMPLEX
(a * (C . c6)) + (((c1) . [a,x]) . c6) is V21() Element of COMPLEX
x . c6 is V21() Element of COMPLEX
a * (x . c6) is V21() Element of COMPLEX
(a * (C . c6)) + (a * (x . c6)) is V21() Element of COMPLEX
(C . c6) + (x . c6) is V21() Element of COMPLEX
a * ((C . c6) + (x . c6)) is V21() Element of COMPLEX
((c1) . (C,x)) . c6 is V21() Element of COMPLEX
a * (((c1) . (C,x)) . c6) is V21() Element of COMPLEX
[a,((c1) . (C,x))] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [a,((c1) . (C,x))] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
((c1) . [a,((c1) . (C,x))]) . c6 is V21() Element of COMPLEX
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] is set
[:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
(c1) is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]

(c1) . (C,x) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[C,x] is set
(c1) . [C,x] is set

(c1) . (x,y) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[x,y] is set
(c1) . [x,y] is set
(c1) . (C,((c1) . (x,y))) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[C,((c1) . (x,y))] is set
(c1) . [C,((c1) . (x,y))] is set
(c1) . (C,y) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[C,y] is set
(c1) . [C,y] is set
(c1) . (((c1) . (C,x)),((c1) . (C,y))) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[((c1) . (C,x)),((c1) . (C,y))] is set
(c1) . [((c1) . (C,x)),((c1) . (C,y))] is set
a is Element of c1
((c1) . (C,((c1) . (x,y)))) . a is V21() Element of COMPLEX
C . a is V21() Element of COMPLEX
((c1) . (x,y)) . a is V21() Element of COMPLEX
(C . a) * (((c1) . (x,y)) . a) is V21() Element of COMPLEX
x . a is V21() Element of COMPLEX
y . a is V21() Element of COMPLEX
(x . a) + (y . a) is V21() Element of COMPLEX
(C . a) * ((x . a) + (y . a)) is V21() Element of COMPLEX
(C . a) * (x . a) is V21() Element of COMPLEX
(C . a) * (y . a) is V21() Element of COMPLEX
((C . a) * (x . a)) + ((C . a) * (y . a)) is V21() Element of COMPLEX
((c1) . (C,x)) . a is V21() Element of COMPLEX
(((c1) . (C,x)) . a) + ((C . a) * (y . a)) is V21() Element of COMPLEX
((c1) . (C,y)) . a is V21() Element of COMPLEX
(((c1) . (C,x)) . a) + (((c1) . (C,y)) . a) is V21() Element of COMPLEX
((c1) . (((c1) . (C,x)),((c1) . (C,y)))) . a is V21() Element of COMPLEX
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] is set
[:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
(c1) is Relation-like [:COMPLEX,(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:COMPLEX,(Funcs (c1,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set

(c1) . (C,x) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[C,x] is set
(c1) . [C,x] is set
y is V21() Element of COMPLEX
[y,C] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]

(c1) . (((c1) . [y,C]),x) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[((c1) . [y,C]),x] is set
(c1) . [((c1) . [y,C]),x] is set
[y,((c1) . (C,x))] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [y,((c1) . (C,x))] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
a is Element of c1
((c1) . (((c1) . [y,C]),x)) . a is V21() Element of COMPLEX
((c1) . [y,C]) . a is V21() Element of COMPLEX
x . a is V21() Element of COMPLEX
(((c1) . [y,C]) . a) * (x . a) is V21() Element of COMPLEX
C . a is V21() Element of COMPLEX
y * (C . a) is V21() Element of COMPLEX
(y * (C . a)) * (x . a) is V21() Element of COMPLEX
(C . a) * (x . a) is V21() Element of COMPLEX
y * ((C . a) * (x . a)) is V21() Element of COMPLEX
((c1) . (C,x)) . a is V21() Element of COMPLEX
y * (((c1) . (C,x)) . a) is V21() Element of COMPLEX
((c1) . [y,((c1) . (C,x))]) . a is V21() Element of COMPLEX
c1 is set
C is non empty set
Funcs (C,COMPLEX) is non empty FUNCTION_DOMAIN of C, COMPLEX
0c is empty V21() Element of COMPLEX
x is set
is set

y is set

IT is set
a . IT is set
f is set
c6 . f is set
0c is empty V21() Element of COMPLEX
c1 is set
C is set
x is non empty set
Funcs (x,COMPLEX) is non empty FUNCTION_DOMAIN of x, COMPLEX
(x) is Relation-like [:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):] -defined Funcs (x,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):]
[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):] is set
[:[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set
bool [:[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set
(x) is Relation-like [:COMPLEX,(Funcs (x,COMPLEX)):] -defined Funcs (x,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):]
[:COMPLEX,(Funcs (x,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set

[:x,REAL:] is set
bool [:x,REAL:] is set

y . C is set
a . C is set
y . c1 is set
a . c1 is set
c6 is V21() Element of COMPLEX
[c6,y] is Element of [:COMPLEX,(Funcs (x,COMPLEX)):]

IT is V21() Element of COMPLEX
[IT,a] is Element of [:COMPLEX,(Funcs (x,COMPLEX)):]

(x) . (((x) . [c6,y]),((x) . [IT,a])) is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
[((x) . [c6,y]),((x) . [IT,a])] is set
(x) . [((x) . [c6,y]),((x) . [IT,a])] is set
h is Element of x
((x) . (((x) . [c6,y]),((x) . [IT,a]))) . h is V21() Element of COMPLEX
((x) . [c6,y]) . h is V21() Element of COMPLEX
((x) . [IT,a]) . h is V21() Element of COMPLEX
(((x) . [c6,y]) . h) + (((x) . [IT,a]) . h) is V21() Element of COMPLEX
y . h is V21() Element of COMPLEX
c6 * (y . h) is V21() Element of COMPLEX
(c6 * (y . h)) + (((x) . [IT,a]) . h) is V21() Element of COMPLEX
IT * 1r is V21() Element of COMPLEX
0c + (IT * 1r) is V21() Element of COMPLEX
f is Element of x
((x) . (((x) . [c6,y]),((x) . [IT,a]))) . f is V21() Element of COMPLEX
((x) . [c6,y]) . f is V21() Element of COMPLEX
((x) . [IT,a]) . f is V21() Element of COMPLEX
(((x) . [c6,y]) . f) + (((x) . [IT,a]) . f) is V21() Element of COMPLEX
y . f is V21() Element of COMPLEX
c6 * (y . f) is V21() Element of COMPLEX
(c6 * (y . f)) + (((x) . [IT,a]) . f) is V21() Element of COMPLEX
IT * 0c is V21() Element of COMPLEX
c6 + (IT * 0c) is V21() Element of COMPLEX
c1 is set
C is set
x is non empty set
Funcs (x,COMPLEX) is non empty FUNCTION_DOMAIN of x, COMPLEX
(x) is Relation-like [:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):] -defined Funcs (x,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):]
[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):] is set
[:[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set
bool [:[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set
(x) is Relation-like [:COMPLEX,(Funcs (x,COMPLEX)):] -defined Funcs (x,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):]
[:COMPLEX,(Funcs (x,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set

[:x,REAL:] is set
bool [:x,REAL:] is set

c6 is V21() Element of COMPLEX
[c6,y] is Element of [:COMPLEX,(Funcs (x,COMPLEX)):]

IT is V21() Element of COMPLEX
[IT,a] is Element of [:COMPLEX,(Funcs (x,COMPLEX)):]

(x) . (((x) . [c6,y]),((x) . [IT,a])) is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
[((x) . [c6,y]),((x) . [IT,a])] is set
(x) . [((x) . [c6,y]),((x) . [IT,a])] is set
c1 is set
C is set
{c1,C} is non empty set
x is non empty set
Funcs (x,COMPLEX) is non empty FUNCTION_DOMAIN of x, COMPLEX
(x) is Relation-like [:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):] -defined Funcs (x,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):]
[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):] is set
[:[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set
bool [:[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set
(x) is Relation-like [:COMPLEX,(Funcs (x,COMPLEX)):] -defined Funcs (x,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):]
[:COMPLEX,(Funcs (x,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set

y . C is set
a . C is set
y . c1 is set
a . c1 is set

IT is Element of x
c6 . IT is V21() Element of COMPLEX
h is V21() Element of COMPLEX
[h,y] is Element of [:COMPLEX,(Funcs (x,COMPLEX)):]

f is Element of x
c6 . f is V21() Element of COMPLEX
t is V21() Element of COMPLEX
[t,a] is Element of [:COMPLEX,(Funcs (x,COMPLEX)):]

(x) . (((x) . [h,y]),((x) . [t,a])) is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
[((x) . [h,y]),((x) . [t,a])] is set
(x) . [((x) . [h,y]),((x) . [t,a])] is set
c11 is Element of x
((x) . (((x) . [h,y]),((x) . [t,a]))) . f is V21() Element of COMPLEX
((x) . [h,y]) . f is V21() Element of COMPLEX
((x) . [t,a]) . f is V21() Element of COMPLEX
(((x) . [h,y]) . f) + (((x) . [t,a]) . f) is V21() Element of COMPLEX
y . f is V21() Element of COMPLEX
h * (y . f) is V21() Element of COMPLEX
(h * (y . f)) + (((x) . [t,a]) . f) is V21() Element of COMPLEX
t * 1r is V21() Element of COMPLEX
0c + (t * 1r) is V21() Element of COMPLEX
((x) . (((x) . [h,y]),((x) . [t,a]))) . IT is V21() Element of COMPLEX
((x) . [h,y]) . IT is V21() Element of COMPLEX
((x) . [t,a]) . IT is V21() Element of COMPLEX
(((x) . [h,y]) . IT) + (((x) . [t,a]) . IT) is V21() Element of COMPLEX
y . IT is V21() Element of COMPLEX
h * (y . IT) is V21() Element of COMPLEX
(h * (y . IT)) + (((x) . [t,a]) . IT) is V21() Element of COMPLEX
t * 0c is V21() Element of COMPLEX
h + (t * 0c) is V21() Element of COMPLEX
c6 . c11 is V21() Element of COMPLEX
((x) . (((x) . [h,y]),((x) . [t,a]))) . c11 is V21() Element of COMPLEX
c1 is set
C is set
{c1,C} is non empty set
x is non empty set
Funcs (x,COMPLEX) is non empty FUNCTION_DOMAIN of x, COMPLEX
(x) is Relation-like [:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):] -defined Funcs (x,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):]
[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):] is set
[:[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set
bool [:[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set
(x) is Relation-like [:COMPLEX,(Funcs (x,COMPLEX)):] -defined Funcs (x,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):]
[:COMPLEX,(Funcs (x,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set

c1 is set
C is set
{c1,C} is non empty set
x is non empty set
Funcs (x,COMPLEX) is non empty FUNCTION_DOMAIN of x, COMPLEX
(x) is Relation-like [:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):] -defined Funcs (x,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):]
[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):] is set
[:[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set
bool [:[:(Funcs (x,COMPLEX)),(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set
(x) is Relation-like [:COMPLEX,(Funcs (x,COMPLEX)):] -defined Funcs (x,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):]
[:COMPLEX,(Funcs (x,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (x,COMPLEX)):],(Funcs (x,COMPLEX)):] is set

[:x,REAL:] is set
bool [:x,REAL:] is set

c6 is V21() Element of COMPLEX
[c6,y] is Element of [:COMPLEX,(Funcs (x,COMPLEX)):]

IT is V21() Element of COMPLEX
[IT,a] is Element of [:COMPLEX,(Funcs (x,COMPLEX)):]

(x) . (((x) . [c6,y]),((x) . [IT,a])) is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
[((x) . [c6,y]),((x) . [IT,a])] is set
(x) . [((x) . [c6,y]),((x) . [IT,a])] is set

c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX

[:c1,REAL:] is set
bool [:c1,REAL:] is set
(c1) is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] is set
[:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
(c1) is Relation-like [:COMPLEX,(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:COMPLEX,(Funcs (c1,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
CLSStruct(# (Funcs (c1,COMPLEX)),(c1),(c1),(c1) #) is non empty strict CLSStruct
c1 is non empty set
(c1) is non empty strict CLSStruct
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX

[:c1,REAL:] is set
bool [:c1,REAL:] is set
(c1) is Relation-like [:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):] is set
[:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:(Funcs (c1,COMPLEX)),(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
(c1) is Relation-like [:COMPLEX,(Funcs (c1,COMPLEX)):] -defined Funcs (c1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):]
[:COMPLEX,(Funcs (c1,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c1,COMPLEX)):],(Funcs (c1,COMPLEX)):] is set
CLSStruct(# (Funcs (c1,COMPLEX)),(c1),(c1),(c1) #) is non empty strict CLSStruct
C is non empty strict CLSStruct
the carrier of C is set
x is