:: CFUNCDOM semantic presentation

NAT is Element of bool REAL
REAL is non empty V37() set
bool REAL is set
COMPLEX is non empty V37() set
RAT is non empty V37() set
INT is non empty V37() set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is set
[:[:NAT,NAT:],NAT:] is set
bool [:[:NAT,NAT:],NAT:] is set
NAT is set
bool NAT is set
bool NAT is set
[:NAT,REAL:] is set
bool [:NAT,REAL:] is set
1 is non empty set
{} is empty set
1r is V21() Element of COMPLEX
addcomplex is Relation-like [:COMPLEX,COMPLEX:] -defined COMPLEX -valued Function-like quasi_total Element of bool [:[:COMPLEX,COMPLEX:],COMPLEX:]
multcomplex is Relation-like [:COMPLEX,COMPLEX:] -defined COMPLEX -valued Function-like quasi_total Element of bool [:[:COMPLEX,COMPLEX:],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 is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
y is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
C . (x,y) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[x,y] is set
C . [x,y] is set
addcomplex .: (x,y) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
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 is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
a is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
C . (y,a) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[y,a] is set
C . [y,a] is set
addcomplex .: (y,a) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
x . (y,a) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
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 is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
y is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
C . (x,y) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[x,y] is set
C . [x,y] is set
multcomplex .: (x,y) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
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 is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
a is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
C . (y,a) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[y,a] is set
C . [y,a] is set
multcomplex .: (y,a) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
x . (y,a) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
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
y is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[x,y] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
C . [x,y] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of 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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
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
a is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[y,a] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
C . [y,a] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of 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] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,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 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[: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 --> 0c is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
c1 is non empty set
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[: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
y is Relation-like c1 -defined C -valued Function-like quasi_total Element of bool [:c1,C:]
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
C is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
x is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
y is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
(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
addcomplex .: (x,y) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
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
C is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
x is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
y is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
(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
multcomplex .: (x,y) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
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
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[: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
C is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
x is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
y is V21() Element of COMPLEX
[y,x] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [y,x] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of 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
C is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
x is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of 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,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
C is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
x is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of 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
y is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
(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
C is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
x is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of 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,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
C is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
x is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of 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
y is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
(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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
C is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
(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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
C is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
(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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
C is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[(- 1r),C] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [(- 1r),C] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
(c1) . (C,((c1) . [(- 1r),C])) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[C,((c1) . [(- 1r),C])] is set
(c1) . [C,((c1) . [(- 1r),C])] is set
x is Element of c1
C . x is V21() Element of COMPLEX
((c1) . (C,((c1) . [(- 1r),C]))) . x is V21() Element of COMPLEX
((c1) . [(- 1r),C]) . x is V21() Element of COMPLEX
(C . x) + (((c1) . [(- 1r),C]) . x) is V21() Element of COMPLEX
(- 1r) * (C . x) is V21() Element of COMPLEX
(C . x) + ((- 1r) * (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
C is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[1r,C] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [1r,C] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of 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
C is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
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)):]
(c1) . [c6,C] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of 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
C is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
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)):]
(c1) . [a,C] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c6 is V21() Element of COMPLEX
[c6,C] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [c6,C] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of 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
C is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
x is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of 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
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)):]
(c1) . [a,C] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[a,x] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [a,x] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of 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)):]
C is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
x is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of 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
y is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
(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
C is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
x is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of 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
y is V21() Element of COMPLEX
[y,C] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [y,C] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of 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
[:C,COMPLEX:] is set
bool [:C,COMPLEX:] is set
x is Relation-like C -defined COMPLEX -valued Function-like quasi_total Element of bool [:C,COMPLEX:]
y is set
y is Relation-like C -defined COMPLEX -valued Function-like quasi_total Element of bool [:C,COMPLEX:]
a is Relation-like C -defined COMPLEX -valued Function-like quasi_total Element of Funcs (C,COMPLEX)
c6 is Relation-like C -defined COMPLEX -valued Function-like quasi_total Element of Funcs (C,COMPLEX)
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) is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
x --> 0 is Relation-like x -defined REAL -valued Function-like quasi_total Element of bool [:x,REAL:]
[:x,REAL:] is set
bool [:x,REAL:] is set
y is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
a is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
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)):]
(x) . [c6,y] is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
IT is V21() Element of COMPLEX
[IT,a] is Element of [:COMPLEX,(Funcs (x,COMPLEX)):]
(x) . [IT,a] is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of 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) is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
x --> 0 is Relation-like x -defined REAL -valued Function-like quasi_total Element of bool [:x,REAL:]
[:x,REAL:] is set
bool [:x,REAL:] is set
y is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
a is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
c6 is V21() Element of COMPLEX
[c6,y] is Element of [:COMPLEX,(Funcs (x,COMPLEX)):]
(x) . [c6,y] is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
IT is V21() Element of COMPLEX
[IT,a] is Element of [:COMPLEX,(Funcs (x,COMPLEX)):]
(x) . [IT,a] is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of 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 is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
a is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
y . C is set
a . C is set
y . c1 is set
a . c1 is set
c6 is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
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)):]
(x) . [h,y] is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of 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) . [t,a] is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of 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
y is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
a is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
c6 is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,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
(x) is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
x --> 0 is Relation-like x -defined REAL -valued Function-like quasi_total Element of bool [:x,REAL:]
[:x,REAL:] is set
bool [:x,REAL:] is set
y is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
a is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
c6 is V21() Element of COMPLEX
[c6,y] is Element of [:COMPLEX,(Funcs (x,COMPLEX)):]
(x) . [c6,y] is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
IT is V21() Element of COMPLEX
[IT,a] is Element of [:COMPLEX,(Funcs (x,COMPLEX)):]
(x) . [IT,a] is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of 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
f is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
c1 is non empty set
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[: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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[: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 Element of the carrier of C
y is Element of the carrier of C
x + y is Element of the carrier of C
the addF of C is Relation-like [: the carrier of C, the carrier of C:] -defined the carrier of C -valued Function-like quasi_total Element of bool [:[: the carrier of C, the carrier of C:], the carrier of C:]
[: the carrier of C, the carrier of C:] is set
[:[: the carrier of C, the carrier of C:], the carrier of C:] is set
bool [:[: the carrier of C, the carrier of C:], the carrier of C:] is set
the addF of C . (x,y) is Element of the carrier of C
[x,y] is set
the addF of C . [x,y] is set
y + x is Element of the carrier of C
the addF of C . (y,x) is Element of the carrier of C
[y,x] is set
the addF of C . [y,x] is set
x is Element of the carrier of C
y is Element of the carrier of C
x + y is Element of the carrier of C
the addF of C is Relation-like [: the carrier of C, the carrier of C:] -defined the carrier of C -valued Function-like quasi_total Element of bool [:[: the carrier of C, the carrier of C:], the carrier of C:]
[: the carrier of C, the carrier of C:] is set
[:[: the carrier of C, the carrier of C:], the carrier of C:] is set
bool [:[: the carrier of C, the carrier of C:], the carrier of C:] is set
the addF of C . (x,y) is Element of the carrier of C
[x,y] is set
the addF of C . [x,y] is set
a is Element of the carrier of C
(x + y) + a is Element of the carrier of C
the addF of C . ((x + y),a) is Element of the carrier of C
[(x + y),a] is set
the addF of C . [(x + y),a] is set
y + a is Element of the carrier of C
the addF of C . (y,a) is Element of the carrier of C
[y,a] is set
the addF of C . [y,a] is set
x + (y + a) is Element of the carrier of C
the addF of C . (x,(y + a)) is Element of the carrier of C
[x,(y + a)] is set
the addF of C . [x,(y + a)] is set
0. C is Element of the carrier of C
the ZeroF of C is Element of the carrier of C
x is Element of the carrier of C
x + (0. C) is Element of the carrier of C
the addF of C is Relation-like [: the carrier of C, the carrier of C:] -defined the carrier of C -valued Function-like quasi_total Element of bool [:[: the carrier of C, the carrier of C:], the carrier of C:]
[: the carrier of C, the carrier of C:] is set
[:[: the carrier of C, the carrier of C:], the carrier of C:] is set
bool [:[: the carrier of C, the carrier of C:], the carrier of C:] is set
the addF of C . (x,(0. C)) is Element of the carrier of C
[x,(0. C)] is set
the addF of C . [x,(0. C)] is set
y is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
(c1) . ((c1),y) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[(c1),y] is set
(c1) . [(c1),y] is set
x is Element of the carrier of C
y is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[(- 1r),y] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [(- 1r),y] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
a is Element of the carrier of C
x + a is Element of the carrier of C
the addF of C is Relation-like [: the carrier of C, the carrier of C:] -defined the carrier of C -valued Function-like quasi_total Element of bool [:[: the carrier of C, the carrier of C:], the carrier of C:]
[: the carrier of C, the carrier of C:] is set
[:[: the carrier of C, the carrier of C:], the carrier of C:] is set
bool [:[: the carrier of C, the carrier of C:], the carrier of C:] is set
the addF of C . (x,a) is Element of the carrier of C
[x,a] is set
the addF of C . [x,a] is set
y is Element of the carrier of C
a is Element of the carrier of C
y + a is Element of the carrier of C
the addF of C is Relation-like [: the carrier of C, the carrier of C:] -defined the carrier of C -valued Function-like quasi_total Element of bool [:[: the carrier of C, the carrier of C:], the carrier of C:]
[: the carrier of C, the carrier of C:] is set
[:[: the carrier of C, the carrier of C:], the carrier of C:] is set
bool [:[: the carrier of C, the carrier of C:], the carrier of C:] is set
the addF of C . (y,a) is Element of the carrier of C
[y,a] is set
the addF of C . [y,a] is set
x is V21() set
x * (y + a) is Element of the carrier of C
the Mult of C is Relation-like [:COMPLEX, the carrier of C:] -defined the carrier of C -valued Function-like quasi_total Element of bool [:[:COMPLEX, the carrier of C:], the carrier of C:]
[:COMPLEX, the carrier of C:] is set
[:[:COMPLEX, the carrier of C:], the carrier of C:] is set
bool [:[:COMPLEX, the carrier of C:], the carrier of C:] is set
[x,(y + a)] is set
the Mult of C . [x,(y + a)] is set
x * y is Element of the carrier of C
[x,y] is set
the Mult of C . [x,y] is set
x * a is Element of the carrier of C
[x,a] is set
the Mult of C . [x,a] is set
(x * y) + (x * a) is Element of the carrier of C
the addF of C . ((x * y),(x * a)) is Element of the carrier of C
[(x * y),(x * a)] is set
the addF of C . [(x * y),(x * a)] is set
a is Element of the carrier of C
x is V21() set
y is V21() set
x + y is V21() Element of COMPLEX
(x + y) * a is Element of the carrier of C
the Mult of C is Relation-like [:COMPLEX, the carrier of C:] -defined the carrier of C -valued Function-like quasi_total Element of bool [:[:COMPLEX, the carrier of C:], the carrier of C:]
[:COMPLEX, the carrier of C:] is set
[:[:COMPLEX, the carrier of C:], the carrier of C:] is set
bool [:[:COMPLEX, the carrier of C:], the carrier of C:] is set
[(x + y),a] is set
the Mult of C . [(x + y),a] is set
x * a is Element of the carrier of C
[x,a] is set
the Mult of C . [x,a] is set
y * a is Element of the carrier of C
[y,a] is set
the Mult of C . [y,a] is set
(x * a) + (y * a) is Element of the carrier of C
the addF of C is Relation-like [: the carrier of C, the carrier of C:] -defined the carrier of C -valued Function-like quasi_total Element of bool [:[: the carrier of C, the carrier of C:], the carrier of C:]
[: the carrier of C, the carrier of C:] is set
[:[: the carrier of C, the carrier of C:], the carrier of C:] is set
bool [:[: the carrier of C, the carrier of C:], the carrier of C:] is set
the addF of C . ((x * a),(y * a)) is Element of the carrier of C
[(x * a),(y * a)] is set
the addF of C . [(x * a),(y * a)] is set
a is Element of the carrier of C
x is V21() set
y is V21() set
x * y is V21() Element of COMPLEX
(x * y) * a is Element of the carrier of C
the Mult of C is Relation-like [:COMPLEX, the carrier of C:] -defined the carrier of C -valued Function-like quasi_total Element of bool [:[:COMPLEX, the carrier of C:], the carrier of C:]
[:COMPLEX, the carrier of C:] is set
[:[:COMPLEX, the carrier of C:], the carrier of C:] is set
bool [:[:COMPLEX, the carrier of C:], the carrier of C:] is set
[(x * y),a] is set
the Mult of C . [(x * y),a] is set
y * a is Element of the carrier of C
[y,a] is set
the Mult of C . [y,a] is set
x * (y * a) is Element of the carrier of C
[x,(y * a)] is set
the Mult of C . [x,(y * a)] is set
x is Element of the carrier of C
1r * x is Element of the carrier of C
the Mult of C is Relation-like [:COMPLEX, the carrier of C:] -defined the carrier of C -valued Function-like quasi_total Element of bool [:[:COMPLEX, the carrier of C:], the carrier of C:]
[:COMPLEX, the carrier of C:] is set
[:[:COMPLEX, the carrier of C:], the carrier of C:] is set
bool [:[:COMPLEX, the carrier of C:], the carrier of C:] is set
[1r,x] is set
the Mult of C . [1r,x] is set
2 is non empty set
{1,2} is non empty set
c1 is non empty set
c1 is non empty set
C is set
x is set
{C,x} is non empty set
c1 is non empty set
C is set
x is set
{C,x} is non empty set
(c1) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
Funcs (c1,COMPLEX) is non empty FUNCTION_DOMAIN of c1, COMPLEX
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[: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
y is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
the carrier of y is set
0. y is right_complementable Element of the carrier of y
the ZeroF of y is right_complementable Element of the carrier of y
a is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c6 is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
IT is right_complementable Element of the carrier of y
f is right_complementable Element of the carrier of y
h is V21() Element of COMPLEX
h * IT is right_complementable Element of the carrier of y
the Mult of y is Relation-like [:COMPLEX, the carrier of y:] -defined the carrier of y -valued Function-like quasi_total Element of bool [:[:COMPLEX, the carrier of y:], the carrier of y:]
[:COMPLEX, the carrier of y:] is set
[:[:COMPLEX, the carrier of y:], the carrier of y:] is set
bool [:[:COMPLEX, the carrier of y:], the carrier of y:] is set
[h,IT] is set
the Mult of y . [h,IT] is set
t is V21() Element of COMPLEX
t * f is right_complementable Element of the carrier of y
[t,f] is set
the Mult of y . [t,f] is set
(h * IT) + (t * f) is right_complementable Element of the carrier of y
the addF of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like quasi_total Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is set
the addF of y . ((h * IT),(t * f)) is right_complementable Element of the carrier of y
[(h * IT),(t * f)] is set
the addF of y . [(h * IT),(t * f)] is set
h is right_complementable Element of the carrier of y
t is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c11 is V21() Element of COMPLEX
[c11,a] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [c11,a] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
b is V21() Element of COMPLEX
[b,c6] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [b,c6] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
(c1) . (((c1) . [c11,a]),((c1) . [b,c6])) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[((c1) . [c11,a]),((c1) . [b,c6])] is set
(c1) . [((c1) . [c11,a]),((c1) . [b,c6])] is set
c11 * IT is right_complementable Element of the carrier of y
the Mult of y is Relation-like [:COMPLEX, the carrier of y:] -defined the carrier of y -valued Function-like quasi_total Element of bool [:[:COMPLEX, the carrier of y:], the carrier of y:]
[:COMPLEX, the carrier of y:] is set
[:[:COMPLEX, the carrier of y:], the carrier of y:] is set
bool [:[:COMPLEX, the carrier of y:], the carrier of y:] is set
[c11,IT] is set
the Mult of y . [c11,IT] is set
b * f is right_complementable Element of the carrier of y
[b,f] is set
the Mult of y . [b,f] is set
(c11 * IT) + (b * f) is right_complementable Element of the carrier of y
the addF of y is Relation-like [: the carrier of y, the carrier of y:] -defined the carrier of y -valued Function-like quasi_total Element of bool [:[: the carrier of y, the carrier of y:], the carrier of y:]
[: the carrier of y, the carrier of y:] is set
[:[: the carrier of y, the carrier of y:], the carrier of y:] is set
bool [:[: the carrier of y, the carrier of y:], the carrier of y:] is set
the addF of y . ((c11 * IT),(b * f)) is right_complementable Element of the carrier of y
[(c11 * IT),(b * f)] is set
the addF of y . [(c11 * IT),(b * f)] 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) 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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
doubleLoopStr(# (Funcs (c1,COMPLEX)),(c1),(c1),(c1),(c1) #) is non empty strict doubleLoopStr
c1 is non empty set
(c1) is doubleLoopStr
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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
doubleLoopStr(# (Funcs (c1,COMPLEX)),(c1),(c1),(c1),(c1) #) is non empty strict doubleLoopStr
c1 is non empty set
(c1) is non empty strict doubleLoopStr
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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
doubleLoopStr(# (Funcs (c1,COMPLEX)),(c1),(c1),(c1),(c1) #) is non empty strict doubleLoopStr
the carrier of (c1) is set
x is Element of the carrier of (c1)
C is Element of the carrier of (c1)
x * C is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the multF of (c1) . (x,C) is Element of the carrier of (c1)
[x,C] is set
the multF of (c1) . [x,C] is set
C * x is Element of the carrier of (c1)
the multF of (c1) . (C,x) is Element of the carrier of (c1)
[C,x] is set
the multF of (c1) . [C,x] is set
c1 is non empty set
(c1) is non empty strict doubleLoopStr
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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
doubleLoopStr(# (Funcs (c1,COMPLEX)),(c1),(c1),(c1),(c1) #) is non empty strict doubleLoopStr
the carrier of (c1) is set
C is Element of the carrier of (c1)
x is Element of the carrier of (c1)
x * C is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the multF of (c1) . (x,C) is Element of the carrier of (c1)
[x,C] is set
the multF of (c1) . [x,C] is set
y is Element of the carrier of (c1)
C * y is Element of the carrier of (c1)
the multF of (c1) . (C,y) is Element of the carrier of (c1)
[C,y] is set
the multF of (c1) . [C,y] is set
c1 is non empty set
(c1) is non empty strict unital doubleLoopStr
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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
doubleLoopStr(# (Funcs (c1,COMPLEX)),(c1),(c1),(c1),(c1) #) is non empty strict doubleLoopStr
the carrier of (c1) is set
0. (c1) is Element of the carrier of (c1)
the ZeroF of (c1) is Element of the carrier of (c1)
1. (c1) is Element of the carrier of (c1)
the OneF of (c1) is Element of the carrier of (c1)
C is Element of the carrier of (c1)
x is Element of the carrier of (c1)
C + x is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the addF of (c1) . (C,x) is Element of the carrier of (c1)
[C,x] is set
the addF of (c1) . [C,x] is set
x + C is Element of the carrier of (c1)
the addF of (c1) . (x,C) is Element of the carrier of (c1)
[x,C] is set
the addF of (c1) . [x,C] is set
y is Element of the carrier of (c1)
(C + x) + y is Element of the carrier of (c1)
the addF of (c1) . ((C + x),y) is Element of the carrier of (c1)
[(C + x),y] is set
the addF of (c1) . [(C + x),y] is set
x + y is Element of the carrier of (c1)
the addF of (c1) . (x,y) is Element of the carrier of (c1)
[x,y] is set
the addF of (c1) . [x,y] is set
C + (x + y) is Element of the carrier of (c1)
the addF of (c1) . (C,(x + y)) is Element of the carrier of (c1)
[C,(x + y)] is set
the addF of (c1) . [C,(x + y)] is set
C + (0. (c1)) is Element of the carrier of (c1)
the addF of (c1) . (C,(0. (c1))) is Element of the carrier of (c1)
[C,(0. (c1))] is set
the addF of (c1) . [C,(0. (c1))] is set
C * x is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
the multF of (c1) . (C,x) is Element of the carrier of (c1)
the multF of (c1) . [C,x] is set
x * C is Element of the carrier of (c1)
the multF of (c1) . (x,C) is Element of the carrier of (c1)
the multF of (c1) . [x,C] is set
(C * x) * y is Element of the carrier of (c1)
the multF of (c1) . ((C * x),y) is Element of the carrier of (c1)
[(C * x),y] is set
the multF of (c1) . [(C * x),y] is set
x * y is Element of the carrier of (c1)
the multF of (c1) . (x,y) is Element of the carrier of (c1)
the multF of (c1) . [x,y] is set
C * (x * y) is Element of the carrier of (c1)
the multF of (c1) . (C,(x * y)) is Element of the carrier of (c1)
[C,(x * y)] is set
the multF of (c1) . [C,(x * y)] is set
C * (1. (c1)) is Element of the carrier of (c1)
the multF of (c1) . (C,(1. (c1))) is Element of the carrier of (c1)
[C,(1. (c1))] is set
the multF of (c1) . [C,(1. (c1))] is set
(1. (c1)) * C is Element of the carrier of (c1)
the multF of (c1) . ((1. (c1)),C) is Element of the carrier of (c1)
[(1. (c1)),C] is set
the multF of (c1) . [(1. (c1)),C] is set
C * (x + y) is Element of the carrier of (c1)
the multF of (c1) . (C,(x + y)) is Element of the carrier of (c1)
the multF of (c1) . [C,(x + y)] is set
C * y is Element of the carrier of (c1)
the multF of (c1) . (C,y) is Element of the carrier of (c1)
[C,y] is set
the multF of (c1) . [C,y] is set
(C * x) + (C * y) is Element of the carrier of (c1)
the addF of (c1) . ((C * x),(C * y)) is Element of the carrier of (c1)
[(C * x),(C * y)] is set
the addF of (c1) . [(C * x),(C * y)] is set
(x + y) * C is Element of the carrier of (c1)
the multF of (c1) . ((x + y),C) is Element of the carrier of (c1)
[(x + y),C] is set
the multF of (c1) . [(x + y),C] is set
y * C is Element of the carrier of (c1)
the multF of (c1) . (y,C) is Element of the carrier of (c1)
[y,C] is set
the multF of (c1) . [y,C] is set
(x * C) + (y * C) is Element of the carrier of (c1)
the addF of (c1) . ((x * C),(y * C)) is Element of the carrier of (c1)
[(x * C),(y * C)] is set
the addF of (c1) . [(x * C),(y * C)] is set
c6 is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
(c1) . ((c1),c6) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[(c1),c6] is set
(c1) . [(c1),c6] 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
[(- 1r),c6] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [(- 1r),c6] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
f is Element of the carrier of (c1)
C + f is Element of the carrier of (c1)
the addF of (c1) . (C,f) is Element of the carrier of (c1)
[C,f] is set
the addF of (c1) . [C,f] is set
(c1) . ((c1),c6) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[(c1),c6] is set
(c1) . [(c1),c6] is set
(x * C) + (C * y) is Element of the carrier of (c1)
the addF of (c1) . ((x * C),(C * y)) is Element of the carrier of (c1)
[(x * C),(C * y)] is set
the addF of (c1) . [(x * C),(C * y)] is set
c1 is non empty set
(c1) is non empty strict unital doubleLoopStr
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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
doubleLoopStr(# (Funcs (c1,COMPLEX)),(c1),(c1),(c1),(c1) #) is non empty strict doubleLoopStr
the carrier of (c1) is set
0. (c1) is Element of the carrier of (c1)
the ZeroF of (c1) is Element of the carrier of (c1)
1. (c1) is Element of the carrier of (c1)
the OneF of (c1) is Element of the carrier of (c1)
C is Element of the carrier of (c1)
x is Element of the carrier of (c1)
C + x is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the addF of (c1) . (C,x) is Element of the carrier of (c1)
[C,x] is set
the addF of (c1) . [C,x] is set
x + C is Element of the carrier of (c1)
the addF of (c1) . (x,C) is Element of the carrier of (c1)
[x,C] is set
the addF of (c1) . [x,C] is set
y is Element of the carrier of (c1)
a is Element of the carrier of (c1)
y + a is Element of the carrier of (c1)
the addF of (c1) . (y,a) is Element of the carrier of (c1)
[y,a] is set
the addF of (c1) . [y,a] is set
c6 is Element of the carrier of (c1)
(y + a) + c6 is Element of the carrier of (c1)
the addF of (c1) . ((y + a),c6) is Element of the carrier of (c1)
[(y + a),c6] is set
the addF of (c1) . [(y + a),c6] is set
a + c6 is Element of the carrier of (c1)
the addF of (c1) . (a,c6) is Element of the carrier of (c1)
[a,c6] is set
the addF of (c1) . [a,c6] is set
y + (a + c6) is Element of the carrier of (c1)
the addF of (c1) . (y,(a + c6)) is Element of the carrier of (c1)
[y,(a + c6)] is set
the addF of (c1) . [y,(a + c6)] is set
IT is Element of the carrier of (c1)
IT + (0. (c1)) is Element of the carrier of (c1)
the addF of (c1) . (IT,(0. (c1))) is Element of the carrier of (c1)
[IT,(0. (c1))] is set
the addF of (c1) . [IT,(0. (c1))] is set
f is Element of the carrier of (c1)
h is Element of the carrier of (c1)
t is Element of the carrier of (c1)
h * t is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
the multF of (c1) . (h,t) is Element of the carrier of (c1)
[h,t] is set
the multF of (c1) . [h,t] is set
t * h is Element of the carrier of (c1)
the multF of (c1) . (t,h) is Element of the carrier of (c1)
[t,h] is set
the multF of (c1) . [t,h] is set
c11 is Element of the carrier of (c1)
b is Element of the carrier of (c1)
c11 * b is Element of the carrier of (c1)
the multF of (c1) . (c11,b) is Element of the carrier of (c1)
[c11,b] is set
the multF of (c1) . [c11,b] is set
c13 is Element of the carrier of (c1)
(c11 * b) * c13 is Element of the carrier of (c1)
the multF of (c1) . ((c11 * b),c13) is Element of the carrier of (c1)
[(c11 * b),c13] is set
the multF of (c1) . [(c11 * b),c13] is set
b * c13 is Element of the carrier of (c1)
the multF of (c1) . (b,c13) is Element of the carrier of (c1)
[b,c13] is set
the multF of (c1) . [b,c13] is set
c11 * (b * c13) is Element of the carrier of (c1)
the multF of (c1) . (c11,(b * c13)) is Element of the carrier of (c1)
[c11,(b * c13)] is set
the multF of (c1) . [c11,(b * c13)] is set
c14 is Element of the carrier of (c1)
c14 * (1. (c1)) is Element of the carrier of (c1)
the multF of (c1) . (c14,(1. (c1))) is Element of the carrier of (c1)
[c14,(1. (c1))] is set
the multF of (c1) . [c14,(1. (c1))] is set
c15 is Element of the carrier of (c1)
(1. (c1)) * c15 is Element of the carrier of (c1)
the multF of (c1) . ((1. (c1)),c15) is Element of the carrier of (c1)
[(1. (c1)),c15] is set
the multF of (c1) . [(1. (c1)),c15] is set
c16 is Element of the carrier of (c1)
c17 is Element of the carrier of (c1)
c18 is Element of the carrier of (c1)
c17 + c18 is Element of the carrier of (c1)
the addF of (c1) . (c17,c18) is Element of the carrier of (c1)
[c17,c18] is set
the addF of (c1) . [c17,c18] is set
c16 * (c17 + c18) is Element of the carrier of (c1)
the multF of (c1) . (c16,(c17 + c18)) is Element of the carrier of (c1)
[c16,(c17 + c18)] is set
the multF of (c1) . [c16,(c17 + c18)] is set
c16 * c17 is Element of the carrier of (c1)
the multF of (c1) . (c16,c17) is Element of the carrier of (c1)
[c16,c17] is set
the multF of (c1) . [c16,c17] is set
c16 * c18 is Element of the carrier of (c1)
the multF of (c1) . (c16,c18) is Element of the carrier of (c1)
[c16,c18] is set
the multF of (c1) . [c16,c18] is set
(c16 * c17) + (c16 * c18) is Element of the carrier of (c1)
the addF of (c1) . ((c16 * c17),(c16 * c18)) is Element of the carrier of (c1)
[(c16 * c17),(c16 * c18)] is set
the addF of (c1) . [(c16 * c17),(c16 * c18)] is set
c20 is Element of the carrier of (c1)
c21 is Element of the carrier of (c1)
c20 + c21 is Element of the carrier of (c1)
the addF of (c1) . (c20,c21) is Element of the carrier of (c1)
[c20,c21] is set
the addF of (c1) . [c20,c21] is set
c19 is Element of the carrier of (c1)
(c20 + c21) * c19 is Element of the carrier of (c1)
the multF of (c1) . ((c20 + c21),c19) is Element of the carrier of (c1)
[(c20 + c21),c19] is set
the multF of (c1) . [(c20 + c21),c19] is set
c20 * c19 is Element of the carrier of (c1)
the multF of (c1) . (c20,c19) is Element of the carrier of (c1)
[c20,c19] is set
the multF of (c1) . [c20,c19] is set
c21 * c19 is Element of the carrier of (c1)
the multF of (c1) . (c21,c19) is Element of the carrier of (c1)
[c21,c19] is set
the multF of (c1) . [c21,c19] is set
(c20 * c19) + (c21 * c19) is Element of the carrier of (c1)
the addF of (c1) . ((c20 * c19),(c21 * c19)) is Element of the carrier of (c1)
[(c20 * c19),(c21 * c19)] is set
the addF of (c1) . [(c20 * c19),(c21 * c19)] is set
the non empty set is non empty set
[: the non empty set , the non empty set :] is set
[:[: the non empty set , the non empty set :], the non empty set :] is set
bool [:[: the non empty set , the non empty set :], the non empty set :] is set
the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :]
[:COMPLEX, the non empty set :] is set
[:[:COMPLEX, the non empty set :], the non empty set :] is set
bool [:[:COMPLEX, the non empty set :], the non empty set :] is set
the Relation-like [:COMPLEX, the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[:COMPLEX, the non empty set :], the non empty set :] is Relation-like [:COMPLEX, the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[:COMPLEX, the non empty set :], the non empty set :]
the Element of the non empty set is Element of the non empty set
( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like [:COMPLEX, the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[:COMPLEX, the non empty set :], the non empty set :], the Element of the non empty set , the Element of the non empty set ) is () ()
the carrier of ( the non empty set , the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like [: the non empty set , the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Relation-like [:COMPLEX, the non empty set :] -defined the non empty set -valued Function-like quasi_total Element of bool [:[:COMPLEX, the non empty set :], the non empty set :], the Element of the non empty set , the Element of the non empty set ) 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) 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) 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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
((Funcs (c1,COMPLEX)),(c1),(c1),(c1),(c1),(c1)) is () ()
c1 is non empty set
(c1) is () ()
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) 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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
((Funcs (c1,COMPLEX)),(c1),(c1),(c1),(c1),(c1)) is () ()
the carrier of (c1) is set
c1 is non empty set
(c1) is non empty () ()
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) 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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
((Funcs (c1,COMPLEX)),(c1),(c1),(c1),(c1),(c1)) is () ()
the carrier of (c1) is set
x is Element of the carrier of (c1)
C is Element of the carrier of (c1)
x * C is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the multF of (c1) . (x,C) is Element of the carrier of (c1)
[x,C] is set
the multF of (c1) . [x,C] is set
C * x is Element of the carrier of (c1)
the multF of (c1) . (C,x) is Element of the carrier of (c1)
[C,x] is set
the multF of (c1) . [C,x] is set
c1 is non empty set
(c1) is non empty () ()
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) 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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
((Funcs (c1,COMPLEX)),(c1),(c1),(c1),(c1),(c1)) is () ()
the carrier of (c1) is set
C is Element of the carrier of (c1)
x is Element of the carrier of (c1)
x * C is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the multF of (c1) . (x,C) is Element of the carrier of (c1)
[x,C] is set
the multF of (c1) . [x,C] is set
y is Element of the carrier of (c1)
C * y is Element of the carrier of (c1)
the multF of (c1) . (C,y) is Element of the carrier of (c1)
[C,y] is set
the multF of (c1) . [C,y] is set
c1 is non empty set
(c1) is non empty unital () ()
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) 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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
((Funcs (c1,COMPLEX)),(c1),(c1),(c1),(c1),(c1)) is () ()
the carrier of (c1) is set
0. (c1) is Element of the carrier of (c1)
the ZeroF of (c1) is Element of the carrier of (c1)
1. (c1) is Element of the carrier of (c1)
the OneF of (c1) is Element of the carrier of (c1)
C is Element of the carrier of (c1)
x is Element of the carrier of (c1)
C + x is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the addF of (c1) . (C,x) is Element of the carrier of (c1)
[C,x] is set
the addF of (c1) . [C,x] is set
x + C is Element of the carrier of (c1)
the addF of (c1) . (x,C) is Element of the carrier of (c1)
[x,C] is set
the addF of (c1) . [x,C] is set
y is Element of the carrier of (c1)
(C + x) + y is Element of the carrier of (c1)
the addF of (c1) . ((C + x),y) is Element of the carrier of (c1)
[(C + x),y] is set
the addF of (c1) . [(C + x),y] is set
x + y is Element of the carrier of (c1)
the addF of (c1) . (x,y) is Element of the carrier of (c1)
[x,y] is set
the addF of (c1) . [x,y] is set
C + (x + y) is Element of the carrier of (c1)
the addF of (c1) . (C,(x + y)) is Element of the carrier of (c1)
[C,(x + y)] is set
the addF of (c1) . [C,(x + y)] is set
C + (0. (c1)) is Element of the carrier of (c1)
the addF of (c1) . (C,(0. (c1))) is Element of the carrier of (c1)
[C,(0. (c1))] is set
the addF of (c1) . [C,(0. (c1))] is set
C * x is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
the multF of (c1) . (C,x) is Element of the carrier of (c1)
the multF of (c1) . [C,x] is set
x * C is Element of the carrier of (c1)
the multF of (c1) . (x,C) is Element of the carrier of (c1)
the multF of (c1) . [x,C] is set
(C * x) * y is Element of the carrier of (c1)
the multF of (c1) . ((C * x),y) is Element of the carrier of (c1)
[(C * x),y] is set
the multF of (c1) . [(C * x),y] is set
x * y is Element of the carrier of (c1)
the multF of (c1) . (x,y) is Element of the carrier of (c1)
the multF of (c1) . [x,y] is set
C * (x * y) is Element of the carrier of (c1)
the multF of (c1) . (C,(x * y)) is Element of the carrier of (c1)
[C,(x * y)] is set
the multF of (c1) . [C,(x * y)] is set
C * (1. (c1)) is Element of the carrier of (c1)
the multF of (c1) . (C,(1. (c1))) is Element of the carrier of (c1)
[C,(1. (c1))] is set
the multF of (c1) . [C,(1. (c1))] is set
C * (x + y) is Element of the carrier of (c1)
the multF of (c1) . (C,(x + y)) is Element of the carrier of (c1)
the multF of (c1) . [C,(x + y)] is set
C * y is Element of the carrier of (c1)
the multF of (c1) . (C,y) is Element of the carrier of (c1)
[C,y] is set
the multF of (c1) . [C,y] is set
(C * x) + (C * y) is Element of the carrier of (c1)
the addF of (c1) . ((C * x),(C * y)) is Element of the carrier of (c1)
[(C * x),(C * y)] is set
the addF of (c1) . [(C * x),(C * y)] is set
a is V21() Element of COMPLEX
a * (C * x) is Element of the carrier of (c1)
the Mult of (c1) is Relation-like [:COMPLEX, the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[:COMPLEX, the carrier of (c1):], the carrier of (c1):]
[:COMPLEX, the carrier of (c1):] is set
[:[:COMPLEX, the carrier of (c1):], the carrier of (c1):] is set
bool [:[:COMPLEX, the carrier of (c1):], the carrier of (c1):] is set
[a,(C * x)] is set
the Mult of (c1) . [a,(C * x)] is set
a * C is Element of the carrier of (c1)
[a,C] is set
the Mult of (c1) . [a,C] is set
(a * C) * x is Element of the carrier of (c1)
the multF of (c1) . ((a * C),x) is Element of the carrier of (c1)
[(a * C),x] is set
the multF of (c1) . [(a * C),x] is set
a * (C + x) is Element of the carrier of (c1)
[a,(C + x)] is set
the Mult of (c1) . [a,(C + x)] is set
a * x is Element of the carrier of (c1)
[a,x] is set
the Mult of (c1) . [a,x] is set
(a * C) + (a * x) is Element of the carrier of (c1)
the addF of (c1) . ((a * C),(a * x)) is Element of the carrier of (c1)
[(a * C),(a * x)] is set
the addF of (c1) . [(a * C),(a * x)] is set
c6 is V21() Element of COMPLEX
a + c6 is V21() Element of COMPLEX
(a + c6) * C is Element of the carrier of (c1)
[(a + c6),C] is set
the Mult of (c1) . [(a + c6),C] is set
c6 * C is Element of the carrier of (c1)
[c6,C] is set
the Mult of (c1) . [c6,C] is set
(a * C) + (c6 * C) is Element of the carrier of (c1)
the addF of (c1) . ((a * C),(c6 * C)) is Element of the carrier of (c1)
[(a * C),(c6 * C)] is set
the addF of (c1) . [(a * C),(c6 * C)] is set
a * c6 is V21() Element of COMPLEX
(a * c6) * C is Element of the carrier of (c1)
[(a * c6),C] is set
the Mult of (c1) . [(a * c6),C] is set
a * (c6 * C) is Element of the carrier of (c1)
[a,(c6 * C)] is set
the Mult of (c1) . [a,(c6 * C)] is set
f is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
(c1) . ((c1),f) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[(c1),f] is set
(c1) . [(c1),f] is set
[(- 1r),f] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [(- 1r),f] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
t is Element of the carrier of (c1)
C + t is Element of the carrier of (c1)
the addF of (c1) . (C,t) is Element of the carrier of (c1)
[C,t] is set
the addF of (c1) . [C,t] is set
(c1) . ((c1),f) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[(c1),f] is set
(c1) . [(c1),f] is set
c1 is non empty set
(c1) is non empty unital () ()
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) 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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
((Funcs (c1,COMPLEX)),(c1),(c1),(c1),(c1),(c1)) is () ()
the carrier of (c1) is set
x is Element of the carrier of (c1)
y is Element of the carrier of (c1)
x + y is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the addF of (c1) . (x,y) is Element of the carrier of (c1)
[x,y] is set
the addF of (c1) . [x,y] is set
y + x is Element of the carrier of (c1)
the addF of (c1) . (y,x) is Element of the carrier of (c1)
[y,x] is set
the addF of (c1) . [y,x] is set
the carrier of (c1) is set
x is Element of the carrier of (c1)
y is Element of the carrier of (c1)
x + y is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the addF of (c1) . (x,y) is Element of the carrier of (c1)
[x,y] is set
the addF of (c1) . [x,y] is set
a is Element of the carrier of (c1)
(x + y) + a is Element of the carrier of (c1)
the addF of (c1) . ((x + y),a) is Element of the carrier of (c1)
[(x + y),a] is set
the addF of (c1) . [(x + y),a] is set
y + a is Element of the carrier of (c1)
the addF of (c1) . (y,a) is Element of the carrier of (c1)
[y,a] is set
the addF of (c1) . [y,a] is set
x + (y + a) is Element of the carrier of (c1)
the addF of (c1) . (x,(y + a)) is Element of the carrier of (c1)
[x,(y + a)] is set
the addF of (c1) . [x,(y + a)] is set
the carrier of (c1) is set
x is Element of the carrier of (c1)
0. (c1) is Element of the carrier of (c1)
the ZeroF of (c1) is Element of the carrier of (c1)
x + (0. (c1)) is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the addF of (c1) . (x,(0. (c1))) is Element of the carrier of (c1)
[x,(0. (c1))] is set
the addF of (c1) . [x,(0. (c1))] is set
y is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
(c1) . ((c1),y) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[(c1),y] is set
(c1) . [(c1),y] is set
the carrier of (c1) is set
x is Element of the carrier of (c1)
y is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[(- 1r),y] is Element of [:COMPLEX,(Funcs (c1,COMPLEX)):]
(c1) . [(- 1r),y] is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
a is Element of the carrier of (c1)
x + a is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the addF of (c1) . (x,a) is Element of the carrier of (c1)
[x,a] is set
the addF of (c1) . [x,a] is set
0. (c1) is Element of the carrier of (c1)
the ZeroF of (c1) is Element of the carrier of (c1)
the carrier of (c1) is set
x is Element of the carrier of (c1)
y is Element of the carrier of (c1)
x * y is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the multF of (c1) . (x,y) is Element of the carrier of (c1)
[x,y] is set
the multF of (c1) . [x,y] is set
y * x is Element of the carrier of (c1)
the multF of (c1) . (y,x) is Element of the carrier of (c1)
[y,x] is set
the multF of (c1) . [y,x] is set
the carrier of (c1) is set
x is Element of the carrier of (c1)
y is Element of the carrier of (c1)
x * y is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the multF of (c1) . (x,y) is Element of the carrier of (c1)
[x,y] is set
the multF of (c1) . [x,y] is set
a is Element of the carrier of (c1)
(x * y) * a is Element of the carrier of (c1)
the multF of (c1) . ((x * y),a) is Element of the carrier of (c1)
[(x * y),a] is set
the multF of (c1) . [(x * y),a] is set
y * a is Element of the carrier of (c1)
the multF of (c1) . (y,a) is Element of the carrier of (c1)
[y,a] is set
the multF of (c1) . [y,a] is set
x * (y * a) is Element of the carrier of (c1)
the multF of (c1) . (x,(y * a)) is Element of the carrier of (c1)
[x,(y * a)] is set
the multF of (c1) . [x,(y * a)] is set
the carrier of (c1) is set
x is Element of the carrier of (c1)
1. (c1) is Element of the carrier of (c1)
the OneF of (c1) is Element of the carrier of (c1)
x * (1. (c1)) is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the multF of (c1) . (x,(1. (c1))) is Element of the carrier of (c1)
[x,(1. (c1))] is set
the multF of (c1) . [x,(1. (c1))] is set
y is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
(c1) . ((c1),y) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
[(c1),y] is set
(c1) . [(c1),y] is set
the carrier of (c1) is set
x is Element of the carrier of (c1)
y is Element of the carrier of (c1)
a is Element of the carrier of (c1)
y + a is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the addF of (c1) . (y,a) is Element of the carrier of (c1)
[y,a] is set
the addF of (c1) . [y,a] is set
x * (y + a) is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
the multF of (c1) . (x,(y + a)) is Element of the carrier of (c1)
[x,(y + a)] is set
the multF of (c1) . [x,(y + a)] is set
x * y is Element of the carrier of (c1)
the multF of (c1) . (x,y) is Element of the carrier of (c1)
[x,y] is set
the multF of (c1) . [x,y] is set
x * a is Element of the carrier of (c1)
the multF of (c1) . (x,a) is Element of the carrier of (c1)
[x,a] is set
the multF of (c1) . [x,a] is set
(x * y) + (x * a) is Element of the carrier of (c1)
the addF of (c1) . ((x * y),(x * a)) is Element of the carrier of (c1)
[(x * y),(x * a)] is set
the addF of (c1) . [(x * y),(x * a)] is set
the carrier of (c1) is set
x is V21() set
y is Element of the carrier of (c1)
a is Element of the carrier of (c1)
y + a is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the addF of (c1) . (y,a) is Element of the carrier of (c1)
[y,a] is set
the addF of (c1) . [y,a] is set
x * (y + a) is Element of the carrier of (c1)
the Mult of (c1) is Relation-like [:COMPLEX, the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[:COMPLEX, the carrier of (c1):], the carrier of (c1):]
[:COMPLEX, the carrier of (c1):] is set
[:[:COMPLEX, the carrier of (c1):], the carrier of (c1):] is set
bool [:[:COMPLEX, the carrier of (c1):], the carrier of (c1):] is set
[x,(y + a)] is set
the Mult of (c1) . [x,(y + a)] is set
x * y is Element of the carrier of (c1)
[x,y] is set
the Mult of (c1) . [x,y] is set
x * a is Element of the carrier of (c1)
[x,a] is set
the Mult of (c1) . [x,a] is set
(x * y) + (x * a) is Element of the carrier of (c1)
the addF of (c1) . ((x * y),(x * a)) is Element of the carrier of (c1)
[(x * y),(x * a)] is set
the addF of (c1) . [(x * y),(x * a)] is set
the carrier of (c1) is set
x is V21() set
y is V21() set
K110(x,y) is V21() set
a is Element of the carrier of (c1)
K110(x,y) * a is Element of the carrier of (c1)
the Mult of (c1) is Relation-like [:COMPLEX, the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[:COMPLEX, the carrier of (c1):], the carrier of (c1):]
[:COMPLEX, the carrier of (c1):] is set
[:[:COMPLEX, the carrier of (c1):], the carrier of (c1):] is set
bool [:[:COMPLEX, the carrier of (c1):], the carrier of (c1):] is set
[K110(x,y),a] is set
the Mult of (c1) . [K110(x,y),a] is set
x * a is Element of the carrier of (c1)
[x,a] is set
the Mult of (c1) . [x,a] is set
y * a is Element of the carrier of (c1)
[y,a] is set
the Mult of (c1) . [y,a] is set
(x * a) + (y * a) is Element of the carrier of (c1)
the addF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the addF of (c1) . ((x * a),(y * a)) is Element of the carrier of (c1)
[(x * a),(y * a)] is set
the addF of (c1) . [(x * a),(y * a)] is set
x + y is V21() Element of COMPLEX
(x + y) * a is Element of the carrier of (c1)
[(x + y),a] is set
the Mult of (c1) . [(x + y),a] is set
the carrier of (c1) is set
x is V21() set
y is V21() set
K111(x,y) is V21() set
a is Element of the carrier of (c1)
K111(x,y) * a is Element of the carrier of (c1)
the Mult of (c1) is Relation-like [:COMPLEX, the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[:COMPLEX, the carrier of (c1):], the carrier of (c1):]
[:COMPLEX, the carrier of (c1):] is set
[:[:COMPLEX, the carrier of (c1):], the carrier of (c1):] is set
bool [:[:COMPLEX, the carrier of (c1):], the carrier of (c1):] is set
[K111(x,y),a] is set
the Mult of (c1) . [K111(x,y),a] is set
y * a is Element of the carrier of (c1)
[y,a] is set
the Mult of (c1) . [y,a] is set
x * (y * a) is Element of the carrier of (c1)
[x,(y * a)] is set
the Mult of (c1) . [x,(y * a)] is set
x * y is V21() Element of COMPLEX
(x * y) * a is Element of the carrier of (c1)
[(x * y),a] is set
the Mult of (c1) . [(x * y),a] is set
the carrier of (c1) is set
x is Element of the carrier of (c1)
y is Element of the carrier of (c1)
x * y is Element of the carrier of (c1)
the multF of (c1) is Relation-like [: the carrier of (c1), the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):]
[: the carrier of (c1), the carrier of (c1):] is set
[:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
bool [:[: the carrier of (c1), the carrier of (c1):], the carrier of (c1):] is set
the multF of (c1) . (x,y) is Element of the carrier of (c1)
[x,y] is set
the multF of (c1) . [x,y] is set
a is V21() Element of COMPLEX
a * (x * y) is Element of the carrier of (c1)
the Mult of (c1) is Relation-like [:COMPLEX, the carrier of (c1):] -defined the carrier of (c1) -valued Function-like quasi_total Element of bool [:[:COMPLEX, the carrier of (c1):], the carrier of (c1):]
[:COMPLEX, the carrier of (c1):] is set
[:[:COMPLEX, the carrier of (c1):], the carrier of (c1):] is set
bool [:[:COMPLEX, the carrier of (c1):], the carrier of (c1):] is set
[a,(x * y)] is set
the Mult of (c1) . [a,(x * y)] is set
a * x is Element of the carrier of (c1)
[a,x] is set
the Mult of (c1) . [a,x] is set
(a * x) * y is Element of the carrier of (c1)
the multF of (c1) . ((a * x),y) is Element of the carrier of (c1)
[(a * x),y] is set
the multF of (c1) . [(a * x),y] is set
(1) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital () () ()
Funcs (1,COMPLEX) is non empty FUNCTION_DOMAIN of 1, COMPLEX
(1) is Relation-like [:(Funcs (1,COMPLEX)),(Funcs (1,COMPLEX)):] -defined Funcs (1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (1,COMPLEX)),(Funcs (1,COMPLEX)):],(Funcs (1,COMPLEX)):]
[:(Funcs (1,COMPLEX)),(Funcs (1,COMPLEX)):] is set
[:[:(Funcs (1,COMPLEX)),(Funcs (1,COMPLEX)):],(Funcs (1,COMPLEX)):] is set
bool [:[:(Funcs (1,COMPLEX)),(Funcs (1,COMPLEX)):],(Funcs (1,COMPLEX)):] is set
(1) is Relation-like [:(Funcs (1,COMPLEX)),(Funcs (1,COMPLEX)):] -defined Funcs (1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (1,COMPLEX)),(Funcs (1,COMPLEX)):],(Funcs (1,COMPLEX)):]
(1) is Relation-like [:COMPLEX,(Funcs (1,COMPLEX)):] -defined Funcs (1,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (1,COMPLEX)):],(Funcs (1,COMPLEX)):]
[:COMPLEX,(Funcs (1,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (1,COMPLEX)):],(Funcs (1,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (1,COMPLEX)):],(Funcs (1,COMPLEX)):] is set
(1) is Relation-like 1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (1,COMPLEX)
1 --> 1r is Relation-like 1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:1,COMPLEX:]
[:1,COMPLEX:] is set
bool [:1,COMPLEX:] is set
(1) is Relation-like 1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (1,COMPLEX)
1 --> 0 is Relation-like 1 -defined REAL -valued Function-like quasi_total Element of bool [:1,REAL:]
[:1,REAL:] is set
bool [:1,REAL:] is set
((Funcs (1,COMPLEX)),(1),(1),(1),(1),(1)) is () ()
c1 is non empty set
(c1) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital () () ()
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) 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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
((Funcs (c1,COMPLEX)),(c1),(c1),(c1),(c1),(c1)) is () ()
c1 is non empty set
(c1) is non empty strict unital doubleLoopStr
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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
doubleLoopStr(# (Funcs (c1,COMPLEX)),(c1),(c1),(c1),(c1) #) is non empty strict doubleLoopStr
1. (c1) is Element of the carrier of (c1)
the carrier of (c1) is set
the OneF of (c1) is Element of the carrier of (c1)
c1 is non empty set
(c1) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital () () ()
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) 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) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 1r is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of bool [:c1,COMPLEX:]
[:c1,COMPLEX:] is set
bool [:c1,COMPLEX:] is set
(c1) is Relation-like c1 -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c1,COMPLEX)
c1 --> 0 is Relation-like c1 -defined REAL -valued Function-like quasi_total Element of bool [:c1,REAL:]
[:c1,REAL:] is set
bool [:c1,REAL:] is set
((Funcs (c1,COMPLEX)),(c1),(c1),(c1),(c1),(c1)) is () ()
1. (c1) is right_complementable Element of the carrier of (c1)
the carrier of (c1) is set
the OneF of (c1) is right_complementable Element of the carrier of (c1)