:: 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:]
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
C is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
x is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
y is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
C . (x,y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[x,y] is set
C . [x,y] is set
addcomplex .: (x,y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
C is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
x is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
y is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
a is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
C . (y,a) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[y,a] is set
C . [y,a] is set
addcomplex .: (y,a) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
x . (y,a) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
x . [y,a] is set
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
C is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
x is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
y is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
C . (x,y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[x,y] is set
C . [x,y] is set
multcomplex .: (x,y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
C is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
x is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
y is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
a is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
C . (y,a) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[y,a] is set
C . [y,a] is set
multcomplex .: (y,a) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
x . (y,a) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
x . [y,a] is set
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
C is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
x is V21() Element of COMPLEX
y is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[x,y] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
C . [x,y] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
a is Element of c₁
(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 (c₁,COMPLEX)
[x,y] is set
C . [x,y] is set
multcomplex [;] (x,y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,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 (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
x is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
y is V21() Element of COMPLEX
a is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[y,a] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
C . [y,a] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₆ is Element of c₁
(C . [y,a]) . c₆ is V21() Element of COMPLEX
a . c₆ is V21() Element of COMPLEX
y * (a . c₆) is V21() Element of COMPLEX
x . [y,a] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(x . [y,a]) . c₆ is V21() Element of COMPLEX
C . (y,a) is Element of Funcs (c₁,COMPLEX)
[y,a] is set
C . [y,a] is set
x . (y,a) is Element of Funcs (c₁,COMPLEX)
x . [y,a] is set
c₁ is non empty set
0 is empty Element of NAT
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
0c is empty V21() Element of COMPLEX
c₁ --> 0c is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
c₁ is non empty set
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
c₁ is non empty set
C is non empty set
[:c₁,C:] is set
bool [:c₁,C:] is set
x is Element of c₁
y is Relation-like c₁ -defined C -valued Function-like quasi_total Element of bool [:c₁,C:]
dom y is set
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
C is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
x is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
y is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . (x,y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[x,y] is set
(c₁) . [x,y] is set
a is Element of c₁
addcomplex .: (x,y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
dom (addcomplex .: (x,y)) is set
((c₁) . (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 c₁
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 c₁
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
c₆ is Element of c₁
C . c₆ is V21() Element of COMPLEX
x . c₆ is V21() Element of COMPLEX
y . c₆ is V21() Element of COMPLEX
(x . c₆) + (y . c₆) is V21() Element of COMPLEX
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
C is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
x is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
y is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . (x,y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[x,y] is set
(c₁) . [x,y] is set
a is Element of c₁
multcomplex .: (x,y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
dom (multcomplex .: (x,y)) is set
((c₁) . (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 c₁
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 c₁
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
c₆ is Element of c₁
C . c₆ is V21() Element of COMPLEX
x . c₆ is V21() Element of COMPLEX
y . c₆ is V21() Element of COMPLEX
(x . c₆) * (y . c₆) is V21() Element of COMPLEX
c₁ is non empty set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
the Element of c₁ is Element of c₁
(c₁) . the Element of c₁ is V21() Element of COMPLEX
0c is empty V21() Element of COMPLEX
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
C is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
x is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
y is V21() Element of COMPLEX
[y,x] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [y,x] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
a is Element of c₁
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 c₁
C . a is V21() Element of COMPLEX
((c₁) . [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 c₁
C . a is V21() Element of COMPLEX
x . a is V21() Element of COMPLEX
y * (x . a) is V21() Element of COMPLEX
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
C is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
x is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . (C,x) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[C,x] is set
(c₁) . [C,x] is set
(c₁) . (x,C) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[x,C] is set
(c₁) . [x,C] is set
y is Element of c₁
((c₁) . (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
((c₁) . (x,C)) . y is V21() Element of COMPLEX
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
C is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
x is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . (C,x) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[C,x] is set
(c₁) . [C,x] is set
y is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . (x,y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[x,y] is set
(c₁) . [x,y] is set
(c₁) . (C,((c₁) . (x,y))) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[C,((c₁) . (x,y))] is set
(c₁) . [C,((c₁) . (x,y))] is set
(c₁) . (((c₁) . (C,x)),y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[((c₁) . (C,x)),y] is set
(c₁) . [((c₁) . (C,x)),y] is set
a is Element of c₁
((c₁) . (C,((c₁) . (x,y)))) . a is V21() Element of COMPLEX
C . a is V21() Element of COMPLEX
((c₁) . (x,y)) . a is V21() Element of COMPLEX
(C . a) + (((c₁) . (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
((c₁) . (C,x)) . a is V21() Element of COMPLEX
(((c₁) . (C,x)) . a) + (y . a) is V21() Element of COMPLEX
((c₁) . (((c₁) . (C,x)),y)) . a is V21() Element of COMPLEX
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
C is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
x is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . (C,x) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[C,x] is set
(c₁) . [C,x] is set
(c₁) . (x,C) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[x,C] is set
(c₁) . [x,C] is set
y is Element of c₁
((c₁) . (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
((c₁) . (x,C)) . y is V21() Element of COMPLEX
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
C is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
x is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . (C,x) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[C,x] is set
(c₁) . [C,x] is set
y is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . (x,y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[x,y] is set
(c₁) . [x,y] is set
(c₁) . (C,((c₁) . (x,y))) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[C,((c₁) . (x,y))] is set
(c₁) . [C,((c₁) . (x,y))] is set
(c₁) . (((c₁) . (C,x)),y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[((c₁) . (C,x)),y] is set
(c₁) . [((c₁) . (C,x)),y] is set
a is Element of c₁
((c₁) . (C,((c₁) . (x,y)))) . a is V21() Element of COMPLEX
C . a is V21() Element of COMPLEX
((c₁) . (x,y)) . a is V21() Element of COMPLEX
(C . a) * (((c₁) . (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
((c₁) . (C,x)) . a is V21() Element of COMPLEX
(((c₁) . (C,x)) . a) * (y . a) is V21() Element of COMPLEX
((c₁) . (((c₁) . (C,x)),y)) . a is V21() Element of COMPLEX
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
C is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . ((c₁),C) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[(c₁),C] is set
(c₁) . [(c₁),C] is set
x is Element of c₁
((c₁) . ((c₁),C)) . x is V21() Element of COMPLEX
(c₁) . x is V21() Element of COMPLEX
C . x is V21() Element of COMPLEX
((c₁) . x) * (C . x) is V21() Element of COMPLEX
1r * (C . x) is V21() Element of COMPLEX
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
C is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . ((c₁),C) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[(c₁),C] is set
(c₁) . [(c₁),C] is set
x is Element of c₁
((c₁) . ((c₁),C)) . x is V21() Element of COMPLEX
(c₁) . x is V21() Element of COMPLEX
C . x is V21() Element of COMPLEX
((c₁) . 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
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
C is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[(- 1r),C] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [(- 1r),C] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . (C,((c₁) . [(- 1r),C])) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[C,((c₁) . [(- 1r),C])] is set
(c₁) . [C,((c₁) . [(- 1r),C])] is set
x is Element of c₁
C . x is V21() Element of COMPLEX
((c₁) . (C,((c₁) . [(- 1r),C]))) . x is V21() Element of COMPLEX
((c₁) . [(- 1r),C]) . x is V21() Element of COMPLEX
(C . x) + (((c₁) . [(- 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
(c₁) . x is V21() Element of COMPLEX
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
C is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[1r,C] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [1r,C] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
x is Element of c₁
((c₁) . [1r,C]) . x is V21() Element of COMPLEX
C . x is V21() Element of COMPLEX
1r * (C . x) is V21() Element of COMPLEX
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
C is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
x is V21() set
y is V21() set
[y,C] is set
(c₁) . [y,C] is set
[x,((c₁) . [y,C])] is set
(c₁) . [x,((c₁) . [y,C])] is set
x * y is V21() Element of COMPLEX
[(x * y),C] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [(x * y),C] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
a is V21() Element of COMPLEX
c₆ is V21() Element of COMPLEX
[c₆,C] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [c₆,C] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[a,((c₁) . [c₆,C])] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [a,((c₁) . [c₆,C])] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
IT is Element of c₁
((c₁) . [a,((c₁) . [c₆,C])]) . IT is V21() Element of COMPLEX
((c₁) . [c₆,C]) . IT is V21() Element of COMPLEX
a * (((c₁) . [c₆,C]) . IT) is V21() Element of COMPLEX
C . IT is V21() Element of COMPLEX
c₆ * (C . IT) is V21() Element of COMPLEX
a * (c₆ * (C . IT)) is V21() Element of COMPLEX
a * c₆ is V21() Element of COMPLEX
(a * c₆) * (C . IT) is V21() Element of COMPLEX
[(a * c₆),C] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [(a * c₆),C] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
((c₁) . [(a * c₆),C]) . IT is V21() Element of COMPLEX
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
C is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
x is V21() set
[x,C] is set
(c₁) . [x,C] is set
y is V21() set
[y,C] is set
(c₁) . [y,C] is set
(c₁) . (((c₁) . [x,C]),((c₁) . [y,C])) is set
[((c₁) . [x,C]),((c₁) . [y,C])] is set
(c₁) . [((c₁) . [x,C]),((c₁) . [y,C])] is set
x + y is V21() Element of COMPLEX
[(x + y),C] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [(x + y),C] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
a is V21() Element of COMPLEX
[a,C] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [a,C] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₆ is V21() Element of COMPLEX
[c₆,C] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [c₆,C] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . (((c₁) . [a,C]),((c₁) . [c₆,C])) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[((c₁) . [a,C]),((c₁) . [c₆,C])] is set
(c₁) . [((c₁) . [a,C]),((c₁) . [c₆,C])] is set
IT is Element of c₁
((c₁) . (((c₁) . [a,C]),((c₁) . [c₆,C]))) . IT is V21() Element of COMPLEX
((c₁) . [a,C]) . IT is V21() Element of COMPLEX
((c₁) . [c₆,C]) . IT is V21() Element of COMPLEX
(((c₁) . [a,C]) . IT) + (((c₁) . [c₆,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)) + (((c₁) . [c₆,C]) . IT) is V21() Element of COMPLEX
c₆ * (C . IT) is V21() Element of COMPLEX
(a * (C . IT)) + (c₆ * (C . IT)) is V21() Element of COMPLEX
a + c₆ is V21() Element of COMPLEX
(a + c₆) * (C . IT) is V21() Element of COMPLEX
[(a + c₆),C] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [(a + c₆),C] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
((c₁) . [(a + c₆),C]) . IT is V21() Element of COMPLEX
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
C is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
x is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . (C,x) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[C,x] is set
(c₁) . [C,x] is set
y is V21() set
[y,C] is set
(c₁) . [y,C] is set
[y,x] is set
(c₁) . [y,x] is set
(c₁) . (((c₁) . [y,C]),((c₁) . [y,x])) is set
[((c₁) . [y,C]),((c₁) . [y,x])] is set
(c₁) . [((c₁) . [y,C]),((c₁) . [y,x])] is set
[y,((c₁) . (C,x))] is set
(c₁) . [y,((c₁) . (C,x))] is set
a is V21() Element of COMPLEX
[a,C] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [a,C] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[a,x] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [a,x] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . (((c₁) . [a,C]),((c₁) . [a,x])) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[((c₁) . [a,C]),((c₁) . [a,x])] is set
(c₁) . [((c₁) . [a,C]),((c₁) . [a,x])] is set
c₆ is Element of c₁
((c₁) . (((c₁) . [a,C]),((c₁) . [a,x]))) . c₆ is V21() Element of COMPLEX
((c₁) . [a,C]) . c₆ is V21() Element of COMPLEX
((c₁) . [a,x]) . c₆ is V21() Element of COMPLEX
(((c₁) . [a,C]) . c₆) + (((c₁) . [a,x]) . c₆) is V21() Element of COMPLEX
C . c₆ is V21() Element of COMPLEX
a * (C . c₆) is V21() Element of COMPLEX
(a * (C . c₆)) + (((c₁) . [a,x]) . c₆) is V21() Element of COMPLEX
x . c₆ is V21() Element of COMPLEX
a * (x . c₆) is V21() Element of COMPLEX
(a * (C . c₆)) + (a * (x . c₆)) is V21() Element of COMPLEX
(C . c₆) + (x . c₆) is V21() Element of COMPLEX
a * ((C . c₆) + (x . c₆)) is V21() Element of COMPLEX
((c₁) . (C,x)) . c₆ is V21() Element of COMPLEX
a * (((c₁) . (C,x)) . c₆) is V21() Element of COMPLEX
[a,((c₁) . (C,x))] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [a,((c₁) . (C,x))] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
((c₁) . [a,((c₁) . (C,x))]) . c₆ is V21() Element of COMPLEX
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
C is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
x is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . (C,x) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[C,x] is set
(c₁) . [C,x] is set
y is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . (x,y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[x,y] is set
(c₁) . [x,y] is set
(c₁) . (C,((c₁) . (x,y))) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[C,((c₁) . (x,y))] is set
(c₁) . [C,((c₁) . (x,y))] is set
(c₁) . (C,y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[C,y] is set
(c₁) . [C,y] is set
(c₁) . (((c₁) . (C,x)),((c₁) . (C,y))) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[((c₁) . (C,x)),((c₁) . (C,y))] is set
(c₁) . [((c₁) . (C,x)),((c₁) . (C,y))] is set
a is Element of c₁
((c₁) . (C,((c₁) . (x,y)))) . a is V21() Element of COMPLEX
C . a is V21() Element of COMPLEX
((c₁) . (x,y)) . a is V21() Element of COMPLEX
(C . a) * (((c₁) . (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
((c₁) . (C,x)) . a is V21() Element of COMPLEX
(((c₁) . (C,x)) . a) + ((C . a) * (y . a)) is V21() Element of COMPLEX
((c₁) . (C,y)) . a is V21() Element of COMPLEX
(((c₁) . (C,x)) . a) + (((c₁) . (C,y)) . a) is V21() Element of COMPLEX
((c₁) . (((c₁) . (C,x)),((c₁) . (C,y)))) . a is V21() Element of COMPLEX
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
C is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
x is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . (C,x) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[C,x] is set
(c₁) . [C,x] is set
y is V21() Element of COMPLEX
[y,C] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [y,C] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . (((c₁) . [y,C]),x) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[((c₁) . [y,C]),x] is set
(c₁) . [((c₁) . [y,C]),x] is set
[y,((c₁) . (C,x))] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [y,((c₁) . (C,x))] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
a is Element of c₁
((c₁) . (((c₁) . [y,C]),x)) . a is V21() Element of COMPLEX
((c₁) . [y,C]) . a is V21() Element of COMPLEX
x . a is V21() Element of COMPLEX
(((c₁) . [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
((c₁) . (C,x)) . a is V21() Element of COMPLEX
y * (((c₁) . (C,x)) . a) is V21() Element of COMPLEX
((c₁) . [y,((c₁) . (C,x))]) . a is V21() Element of COMPLEX
c₁ 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)
c₆ 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
c₆ . f is set
0c is empty V21() Element of COMPLEX
c₁ 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 . c₁ is set
a . c₁ is set
c₆ is V21() Element of COMPLEX
[c₆,y] is Element of [:COMPLEX,(Funcs (x,COMPLEX)):]
(x) . [c₆,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) . [c₆,y]),((x) . [IT,a])) is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
[((x) . [c₆,y]),((x) . [IT,a])] is set
(x) . [((x) . [c₆,y]),((x) . [IT,a])] is set
h is Element of x
((x) . (((x) . [c₆,y]),((x) . [IT,a]))) . h is V21() Element of COMPLEX
((x) . [c₆,y]) . h is V21() Element of COMPLEX
((x) . [IT,a]) . h is V21() Element of COMPLEX
(((x) . [c₆,y]) . h) + (((x) . [IT,a]) . h) is V21() Element of COMPLEX
y . h is V21() Element of COMPLEX
c₆ * (y . h) is V21() Element of COMPLEX
(c₆ * (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) . [c₆,y]),((x) . [IT,a]))) . f is V21() Element of COMPLEX
((x) . [c₆,y]) . f is V21() Element of COMPLEX
((x) . [IT,a]) . f is V21() Element of COMPLEX
(((x) . [c₆,y]) . f) + (((x) . [IT,a]) . f) is V21() Element of COMPLEX
y . f is V21() Element of COMPLEX
c₆ * (y . f) is V21() Element of COMPLEX
(c₆ * (y . f)) + (((x) . [IT,a]) . f) is V21() Element of COMPLEX
IT * 0c is V21() Element of COMPLEX
c₆ + (IT * 0c) is V21() Element of COMPLEX
c₁ 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)
c₆ is V21() Element of COMPLEX
[c₆,y] is Element of [:COMPLEX,(Funcs (x,COMPLEX)):]
(x) . [c₆,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) . [c₆,y]),((x) . [IT,a])) is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
[((x) . [c₆,y]),((x) . [IT,a])] is set
(x) . [((x) . [c₆,y]),((x) . [IT,a])] is set
c₁ is set
C is set
{c₁,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 . c₁ is set
a . c₁ is set
c₆ is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
IT is Element of x
c₆ . 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
c₆ . 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
c₁₁ 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
c₆ . c₁₁ is V21() Element of COMPLEX
((x) . (((x) . [h,y]),((x) . [t,a]))) . c₁₁ is V21() Element of COMPLEX
c₁ is set
C is set
{c₁,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)
c₆ is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
c₁ is set
C is set
{c₁,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)
c₆ is V21() Element of COMPLEX
[c₆,y] is Element of [:COMPLEX,(Funcs (x,COMPLEX)):]
(x) . [c₆,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) . [c₆,y]),((x) . [IT,a])) is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
[((x) . [c₆,y]),((x) . [IT,a])] is set
(x) . [((x) . [c₆,y]),((x) . [IT,a])] is set
f is Relation-like x -defined COMPLEX -valued Function-like quasi_total Element of Funcs (x,COMPLEX)
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
CLSStruct(# (Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁) #) is non empty strict CLSStruct
c₁ is non empty set
(c₁) is non empty strict CLSStruct
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
CLSStruct(# (Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁) #) 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 c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . ((c₁),y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[(c₁),y] is set
(c₁) . [(c₁),y] is set
x is Element of the carrier of C
y is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[(- 1r),y] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [(- 1r),y] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,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
c₁ is non empty set
c₁ is non empty set
C is set
x is set
{C,x} is non empty set
c₁ is non empty set
C is set
x is set
{C,x} is non empty set
(c₁) is non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
CLSStruct(# (Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁) #) 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 c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₆ is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,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 c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁₁ is V21() Element of COMPLEX
[c₁₁,a] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [c₁₁,a] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
b is V21() Element of COMPLEX
[b,c₆] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [b,c₆] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . (((c₁) . [c₁₁,a]),((c₁) . [b,c₆])) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[((c₁) . [c₁₁,a]),((c₁) . [b,c₆])] is set
(c₁) . [((c₁) . [c₁₁,a]),((c₁) . [b,c₆])] is set
c₁₁ * 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
[c₁₁,IT] is set
the Mult of y . [c₁₁,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
(c₁₁ * 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 . ((c₁₁ * IT),(b * f)) is right_complementable Element of the carrier of y
[(c₁₁ * IT),(b * f)] is set
the addF of y . [(c₁₁ * IT),(b * f)] is set
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
doubleLoopStr(# (Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁),(c₁) #) is non empty strict doubleLoopStr
c₁ is non empty set
(c₁) is doubleLoopStr
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
doubleLoopStr(# (Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁),(c₁) #) is non empty strict doubleLoopStr
c₁ is non empty set
(c₁) is non empty strict doubleLoopStr
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
doubleLoopStr(# (Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁),(c₁) #) is non empty strict doubleLoopStr
the carrier of (c₁) is set
x is Element of the carrier of (c₁)
C is Element of the carrier of (c₁)
x * C is Element of the carrier of (c₁)
the multF 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 multF of (c₁) . (x,C) is Element of the carrier of (c₁)
[x,C] is set
the multF of (c₁) . [x,C] is set
C * x is Element of the carrier of (c₁)
the multF of (c₁) . (C,x) is Element of the carrier of (c₁)
[C,x] is set
the multF of (c₁) . [C,x] is set
c₁ is non empty set
(c₁) is non empty strict doubleLoopStr
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
doubleLoopStr(# (Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁),(c₁) #) is non empty strict doubleLoopStr
the carrier of (c₁) is set
C is Element of the carrier of (c₁)
x is Element of the carrier of (c₁)
x * C is Element of the carrier of (c₁)
the multF 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 multF of (c₁) . (x,C) is Element of the carrier of (c₁)
[x,C] is set
the multF of (c₁) . [x,C] is set
y is Element of the carrier of (c₁)
C * y is Element of the carrier of (c₁)
the multF of (c₁) . (C,y) is Element of the carrier of (c₁)
[C,y] is set
the multF of (c₁) . [C,y] is set
c₁ is non empty set
(c₁) is non empty strict unital doubleLoopStr
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
doubleLoopStr(# (Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁),(c₁) #) is non empty strict doubleLoopStr
the carrier of (c₁) is set
0. (c₁) is Element of the carrier of (c₁)
the ZeroF of (c₁) is Element of the carrier of (c₁)
1. (c₁) is Element of the carrier of (c₁)
the OneF of (c₁) is Element of the carrier of (c₁)
C is Element of the carrier of (c₁)
x is Element of the carrier of (c₁)
C + x 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₁) . (C,x) is Element of the carrier of (c₁)
[C,x] is set
the addF of (c₁) . [C,x] is set
x + C is Element of the carrier of (c₁)
the addF of (c₁) . (x,C) is Element of the carrier of (c₁)
[x,C] is set
the addF of (c₁) . [x,C] is set
y is Element of the carrier of (c₁)
(C + x) + y is Element of the carrier of (c₁)
the addF of (c₁) . ((C + x),y) is Element of the carrier of (c₁)
[(C + x),y] is set
the addF of (c₁) . [(C + x),y] is set
x + y is Element of the carrier of (c₁)
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
C + (x + y) is Element of the carrier of (c₁)
the addF of (c₁) . (C,(x + y)) is Element of the carrier of (c₁)
[C,(x + y)] is set
the addF of (c₁) . [C,(x + y)] is set
C + (0. (c₁)) is Element of the carrier of (c₁)
the addF of (c₁) . (C,(0. (c₁))) is Element of the carrier of (c₁)
[C,(0. (c₁))] is set
the addF of (c₁) . [C,(0. (c₁))] is set
C * x is Element of the carrier of (c₁)
the multF 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 multF of (c₁) . (C,x) is Element of the carrier of (c₁)
the multF of (c₁) . [C,x] is set
x * C is Element of the carrier of (c₁)
the multF of (c₁) . (x,C) is Element of the carrier of (c₁)
the multF of (c₁) . [x,C] is set
(C * x) * y is Element of the carrier of (c₁)
the multF of (c₁) . ((C * x),y) is Element of the carrier of (c₁)
[(C * x),y] is set
the multF of (c₁) . [(C * x),y] is set
x * y is Element of the carrier of (c₁)
the multF of (c₁) . (x,y) is Element of the carrier of (c₁)
the multF of (c₁) . [x,y] is set
C * (x * y) is Element of the carrier of (c₁)
the multF of (c₁) . (C,(x * y)) is Element of the carrier of (c₁)
[C,(x * y)] is set
the multF of (c₁) . [C,(x * y)] is set
C * (1. (c₁)) is Element of the carrier of (c₁)
the multF of (c₁) . (C,(1. (c₁))) is Element of the carrier of (c₁)
[C,(1. (c₁))] is set
the multF of (c₁) . [C,(1. (c₁))] is set
(1. (c₁)) * C is Element of the carrier of (c₁)
the multF of (c₁) . ((1. (c₁)),C) is Element of the carrier of (c₁)
[(1. (c₁)),C] is set
the multF of (c₁) . [(1. (c₁)),C] is set
C * (x + y) is Element of the carrier of (c₁)
the multF of (c₁) . (C,(x + y)) is Element of the carrier of (c₁)
the multF of (c₁) . [C,(x + y)] is set
C * y is Element of the carrier of (c₁)
the multF of (c₁) . (C,y) is Element of the carrier of (c₁)
[C,y] is set
the multF of (c₁) . [C,y] is set
(C * x) + (C * y) is Element of the carrier of (c₁)
the addF of (c₁) . ((C * x),(C * y)) is Element of the carrier of (c₁)
[(C * x),(C * y)] is set
the addF of (c₁) . [(C * x),(C * y)] is set
(x + y) * C is Element of the carrier of (c₁)
the multF of (c₁) . ((x + y),C) is Element of the carrier of (c₁)
[(x + y),C] is set
the multF of (c₁) . [(x + y),C] is set
y * C is Element of the carrier of (c₁)
the multF of (c₁) . (y,C) is Element of the carrier of (c₁)
[y,C] is set
the multF of (c₁) . [y,C] is set
(x * C) + (y * C) is Element of the carrier of (c₁)
the addF of (c₁) . ((x * C),(y * C)) is Element of the carrier of (c₁)
[(x * C),(y * C)] is set
the addF of (c₁) . [(x * C),(y * C)] is set
c₆ is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . ((c₁),c₆) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[(c₁),c₆] is set
(c₁) . [(c₁),c₆] is set
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
[(- 1r),c₆] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [(- 1r),c₆] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
f is Element of the carrier of (c₁)
C + f is Element of the carrier of (c₁)
the addF of (c₁) . (C,f) is Element of the carrier of (c₁)
[C,f] is set
the addF of (c₁) . [C,f] is set
(c₁) . ((c₁),c₆) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[(c₁),c₆] is set
(c₁) . [(c₁),c₆] is set
(x * C) + (C * y) is Element of the carrier of (c₁)
the addF of (c₁) . ((x * C),(C * y)) is Element of the carrier of (c₁)
[(x * C),(C * y)] is set
the addF of (c₁) . [(x * C),(C * y)] is set
c₁ is non empty set
(c₁) is non empty strict unital doubleLoopStr
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
doubleLoopStr(# (Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁),(c₁) #) is non empty strict doubleLoopStr
the carrier of (c₁) is set
0. (c₁) is Element of the carrier of (c₁)
the ZeroF of (c₁) is Element of the carrier of (c₁)
1. (c₁) is Element of the carrier of (c₁)
the OneF of (c₁) is Element of the carrier of (c₁)
C is Element of the carrier of (c₁)
x is Element of the carrier of (c₁)
C + x 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₁) . (C,x) is Element of the carrier of (c₁)
[C,x] is set
the addF of (c₁) . [C,x] is set
x + C is Element of the carrier of (c₁)
the addF of (c₁) . (x,C) is Element of the carrier of (c₁)
[x,C] is set
the addF of (c₁) . [x,C] 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₁) . (y,a) is Element of the carrier of (c₁)
[y,a] is set
the addF of (c₁) . [y,a] is set
c₆ is Element of the carrier of (c₁)
(y + a) + c₆ is Element of the carrier of (c₁)
the addF of (c₁) . ((y + a),c₆) is Element of the carrier of (c₁)
[(y + a),c₆] is set
the addF of (c₁) . [(y + a),c₆] is set
a + c₆ is Element of the carrier of (c₁)
the addF of (c₁) . (a,c₆) is Element of the carrier of (c₁)
[a,c₆] is set
the addF of (c₁) . [a,c₆] is set
y + (a + c₆) is Element of the carrier of (c₁)
the addF of (c₁) . (y,(a + c₆)) is Element of the carrier of (c₁)
[y,(a + c₆)] is set
the addF of (c₁) . [y,(a + c₆)] is set
IT is Element of the carrier of (c₁)
IT + (0. (c₁)) is Element of the carrier of (c₁)
the addF of (c₁) . (IT,(0. (c₁))) is Element of the carrier of (c₁)
[IT,(0. (c₁))] is set
the addF of (c₁) . [IT,(0. (c₁))] is set
f is Element of the carrier of (c₁)
h is Element of the carrier of (c₁)
t is Element of the carrier of (c₁)
h * t is Element of the carrier of (c₁)
the multF 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 multF of (c₁) . (h,t) is Element of the carrier of (c₁)
[h,t] is set
the multF of (c₁) . [h,t] is set
t * h is Element of the carrier of (c₁)
the multF of (c₁) . (t,h) is Element of the carrier of (c₁)
[t,h] is set
the multF of (c₁) . [t,h] is set
c₁₁ is Element of the carrier of (c₁)
b is Element of the carrier of (c₁)
c₁₁ * b is Element of the carrier of (c₁)
the multF of (c₁) . (c₁₁,b) is Element of the carrier of (c₁)
[c₁₁,b] is set
the multF of (c₁) . [c₁₁,b] is set
c₁₃ is Element of the carrier of (c₁)
(c₁₁ * b) * c₁₃ is Element of the carrier of (c₁)
the multF of (c₁) . ((c₁₁ * b),c₁₃) is Element of the carrier of (c₁)
[(c₁₁ * b),c₁₃] is set
the multF of (c₁) . [(c₁₁ * b),c₁₃] is set
b * c₁₃ is Element of the carrier of (c₁)
the multF of (c₁) . (b,c₁₃) is Element of the carrier of (c₁)
[b,c₁₃] is set
the multF of (c₁) . [b,c₁₃] is set
c₁₁ * (b * c₁₃) is Element of the carrier of (c₁)
the multF of (c₁) . (c₁₁,(b * c₁₃)) is Element of the carrier of (c₁)
[c₁₁,(b * c₁₃)] is set
the multF of (c₁) . [c₁₁,(b * c₁₃)] is set
c₁₄ is Element of the carrier of (c₁)
c₁₄ * (1. (c₁)) is Element of the carrier of (c₁)
the multF of (c₁) . (c₁₄,(1. (c₁))) is Element of the carrier of (c₁)
[c₁₄,(1. (c₁))] is set
the multF of (c₁) . [c₁₄,(1. (c₁))] is set
c₁₅ is Element of the carrier of (c₁)
(1. (c₁)) * c₁₅ is Element of the carrier of (c₁)
the multF of (c₁) . ((1. (c₁)),c₁₅) is Element of the carrier of (c₁)
[(1. (c₁)),c₁₅] is set
the multF of (c₁) . [(1. (c₁)),c₁₅] is set
c₁₆ is Element of the carrier of (c₁)
c₁₇ is Element of the carrier of (c₁)
c₁₈ is Element of the carrier of (c₁)
c₁₇ + c₁₈ is Element of the carrier of (c₁)
the addF of (c₁) . (c₁₇,c₁₈) is Element of the carrier of (c₁)
[c₁₇,c₁₈] is set
the addF of (c₁) . [c₁₇,c₁₈] is set
c₁₆ * (c₁₇ + c₁₈) is Element of the carrier of (c₁)
the multF of (c₁) . (c₁₆,(c₁₇ + c₁₈)) is Element of the carrier of (c₁)
[c₁₆,(c₁₇ + c₁₈)] is set
the multF of (c₁) . [c₁₆,(c₁₇ + c₁₈)] is set
c₁₆ * c₁₇ is Element of the carrier of (c₁)
the multF of (c₁) . (c₁₆,c₁₇) is Element of the carrier of (c₁)
[c₁₆,c₁₇] is set
the multF of (c₁) . [c₁₆,c₁₇] is set
c₁₆ * c₁₈ is Element of the carrier of (c₁)
the multF of (c₁) . (c₁₆,c₁₈) is Element of the carrier of (c₁)
[c₁₆,c₁₈] is set
the multF of (c₁) . [c₁₆,c₁₈] is set
(c₁₆ * c₁₇) + (c₁₆ * c₁₈) is Element of the carrier of (c₁)
the addF of (c₁) . ((c₁₆ * c₁₇),(c₁₆ * c₁₈)) is Element of the carrier of (c₁)
[(c₁₆ * c₁₇),(c₁₆ * c₁₈)] is set
the addF of (c₁) . [(c₁₆ * c₁₇),(c₁₆ * c₁₈)] is set
c₂₀ is Element of the carrier of (c₁)
c₂₁ is Element of the carrier of (c₁)
c₂₀ + c₂₁ is Element of the carrier of (c₁)
the addF of (c₁) . (c₂₀,c₂₁) is Element of the carrier of (c₁)
[c₂₀,c₂₁] is set
the addF of (c₁) . [c₂₀,c₂₁] is set
c₁₉ is Element of the carrier of (c₁)
(c₂₀ + c₂₁) * c₁₉ is Element of the carrier of (c₁)
the multF of (c₁) . ((c₂₀ + c₂₁),c₁₉) is Element of the carrier of (c₁)
[(c₂₀ + c₂₁),c₁₉] is set
the multF of (c₁) . [(c₂₀ + c₂₁),c₁₉] is set
c₂₀ * c₁₉ is Element of the carrier of (c₁)
the multF of (c₁) . (c₂₀,c₁₉) is Element of the carrier of (c₁)
[c₂₀,c₁₉] is set
the multF of (c₁) . [c₂₀,c₁₉] is set
c₂₁ * c₁₉ is Element of the carrier of (c₁)
the multF of (c₁) . (c₂₁,c₁₉) is Element of the carrier of (c₁)
[c₂₁,c₁₉] is set
the multF of (c₁) . [c₂₁,c₁₉] is set
(c₂₀ * c₁₉) + (c₂₁ * c₁₉) is Element of the carrier of (c₁)
the addF of (c₁) . ((c₂₀ * c₁₉),(c₂₁ * c₁₉)) is Element of the carrier of (c₁)
[(c₂₀ * c₁₉),(c₂₁ * c₁₉)] is set
the addF of (c₁) . [(c₂₀ * c₁₉),(c₂₁ * c₁₉)] 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
c₁ is non empty set
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
((Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁),(c₁),(c₁)) is () ()
c₁ is non empty set
(c₁) is () ()
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
((Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁),(c₁),(c₁)) is () ()
the carrier of (c₁) is set
c₁ is non empty set
(c₁) is non empty () ()
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
((Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁),(c₁),(c₁)) is () ()
the carrier of (c₁) is set
x is Element of the carrier of (c₁)
C is Element of the carrier of (c₁)
x * C is Element of the carrier of (c₁)
the multF 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 multF of (c₁) . (x,C) is Element of the carrier of (c₁)
[x,C] is set
the multF of (c₁) . [x,C] is set
C * x is Element of the carrier of (c₁)
the multF of (c₁) . (C,x) is Element of the carrier of (c₁)
[C,x] is set
the multF of (c₁) . [C,x] is set
c₁ is non empty set
(c₁) is non empty () ()
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
((Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁),(c₁),(c₁)) is () ()
the carrier of (c₁) is set
C is Element of the carrier of (c₁)
x is Element of the carrier of (c₁)
x * C is Element of the carrier of (c₁)
the multF 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 multF of (c₁) . (x,C) is Element of the carrier of (c₁)
[x,C] is set
the multF of (c₁) . [x,C] is set
y is Element of the carrier of (c₁)
C * y is Element of the carrier of (c₁)
the multF of (c₁) . (C,y) is Element of the carrier of (c₁)
[C,y] is set
the multF of (c₁) . [C,y] is set
c₁ is non empty set
(c₁) is non empty unital () ()
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
((Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁),(c₁),(c₁)) is () ()
the carrier of (c₁) is set
0. (c₁) is Element of the carrier of (c₁)
the ZeroF of (c₁) is Element of the carrier of (c₁)
1. (c₁) is Element of the carrier of (c₁)
the OneF of (c₁) is Element of the carrier of (c₁)
C is Element of the carrier of (c₁)
x is Element of the carrier of (c₁)
C + x 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₁) . (C,x) is Element of the carrier of (c₁)
[C,x] is set
the addF of (c₁) . [C,x] is set
x + C is Element of the carrier of (c₁)
the addF of (c₁) . (x,C) is Element of the carrier of (c₁)
[x,C] is set
the addF of (c₁) . [x,C] is set
y is Element of the carrier of (c₁)
(C + x) + y is Element of the carrier of (c₁)
the addF of (c₁) . ((C + x),y) is Element of the carrier of (c₁)
[(C + x),y] is set
the addF of (c₁) . [(C + x),y] is set
x + y is Element of the carrier of (c₁)
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
C + (x + y) is Element of the carrier of (c₁)
the addF of (c₁) . (C,(x + y)) is Element of the carrier of (c₁)
[C,(x + y)] is set
the addF of (c₁) . [C,(x + y)] is set
C + (0. (c₁)) is Element of the carrier of (c₁)
the addF of (c₁) . (C,(0. (c₁))) is Element of the carrier of (c₁)
[C,(0. (c₁))] is set
the addF of (c₁) . [C,(0. (c₁))] is set
C * x is Element of the carrier of (c₁)
the multF 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 multF of (c₁) . (C,x) is Element of the carrier of (c₁)
the multF of (c₁) . [C,x] is set
x * C is Element of the carrier of (c₁)
the multF of (c₁) . (x,C) is Element of the carrier of (c₁)
the multF of (c₁) . [x,C] is set
(C * x) * y is Element of the carrier of (c₁)
the multF of (c₁) . ((C * x),y) is Element of the carrier of (c₁)
[(C * x),y] is set
the multF of (c₁) . [(C * x),y] is set
x * y is Element of the carrier of (c₁)
the multF of (c₁) . (x,y) is Element of the carrier of (c₁)
the multF of (c₁) . [x,y] is set
C * (x * y) is Element of the carrier of (c₁)
the multF of (c₁) . (C,(x * y)) is Element of the carrier of (c₁)
[C,(x * y)] is set
the multF of (c₁) . [C,(x * y)] is set
C * (1. (c₁)) is Element of the carrier of (c₁)
the multF of (c₁) . (C,(1. (c₁))) is Element of the carrier of (c₁)
[C,(1. (c₁))] is set
the multF of (c₁) . [C,(1. (c₁))] is set
C * (x + y) is Element of the carrier of (c₁)
the multF of (c₁) . (C,(x + y)) is Element of the carrier of (c₁)
the multF of (c₁) . [C,(x + y)] is set
C * y is Element of the carrier of (c₁)
the multF of (c₁) . (C,y) is Element of the carrier of (c₁)
[C,y] is set
the multF of (c₁) . [C,y] is set
(C * x) + (C * y) is Element of the carrier of (c₁)
the addF of (c₁) . ((C * x),(C * y)) is Element of the carrier of (c₁)
[(C * x),(C * y)] is set
the addF of (c₁) . [(C * x),(C * y)] is set
a is V21() Element of COMPLEX
a * (C * 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
[a,(C * x)] is set
the Mult of (c₁) . [a,(C * x)] is set
a * C is Element of the carrier of (c₁)
[a,C] is set
the Mult of (c₁) . [a,C] is set
(a * C) * x is Element of the carrier of (c₁)
the multF of (c₁) . ((a * C),x) is Element of the carrier of (c₁)
[(a * C),x] is set
the multF of (c₁) . [(a * C),x] is set
a * (C + x) is Element of the carrier of (c₁)
[a,(C + x)] is set
the Mult of (c₁) . [a,(C + x)] is set
a * x is Element of the carrier of (c₁)
[a,x] is set
the Mult of (c₁) . [a,x] is set
(a * C) + (a * x) is Element of the carrier of (c₁)
the addF of (c₁) . ((a * C),(a * x)) is Element of the carrier of (c₁)
[(a * C),(a * x)] is set
the addF of (c₁) . [(a * C),(a * x)] is set
c₆ is V21() Element of COMPLEX
a + c₆ is V21() Element of COMPLEX
(a + c₆) * C is Element of the carrier of (c₁)
[(a + c₆),C] is set
the Mult of (c₁) . [(a + c₆),C] is set
c₆ * C is Element of the carrier of (c₁)
[c₆,C] is set
the Mult of (c₁) . [c₆,C] is set
(a * C) + (c₆ * C) is Element of the carrier of (c₁)
the addF of (c₁) . ((a * C),(c₆ * C)) is Element of the carrier of (c₁)
[(a * C),(c₆ * C)] is set
the addF of (c₁) . [(a * C),(c₆ * C)] is set
a * c₆ is V21() Element of COMPLEX
(a * c₆) * C is Element of the carrier of (c₁)
[(a * c₆),C] is set
the Mult of (c₁) . [(a * c₆),C] is set
a * (c₆ * C) is Element of the carrier of (c₁)
[a,(c₆ * C)] is set
the Mult of (c₁) . [a,(c₆ * C)] is set
f is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . ((c₁),f) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[(c₁),f] is set
(c₁) . [(c₁),f] is set
[(- 1r),f] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [(- 1r),f] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
t is Element of the carrier of (c₁)
C + t is Element of the carrier of (c₁)
the addF of (c₁) . (C,t) is Element of the carrier of (c₁)
[C,t] is set
the addF of (c₁) . [C,t] is set
(c₁) . ((c₁),f) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[(c₁),f] is set
(c₁) . [(c₁),f] is set
c₁ is non empty set
(c₁) is non empty unital () ()
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
((Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁),(c₁),(c₁)) is () ()
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
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
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
the carrier of (c₁) is set
x is Element of the carrier of (c₁)
0. (c₁) is Element of the carrier of (c₁)
the ZeroF of (c₁) 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 c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . ((c₁),y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[(c₁),y] is set
(c₁) . [(c₁),y] is set
the carrier of (c₁) is set
x is Element of the carrier of (c₁)
y is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[(- 1r),y] is Element of [:COMPLEX,(Funcs (c₁,COMPLEX)):]
(c₁) . [(- 1r),y] is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,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
0. (c₁) is Element of the carrier of (c₁)
the ZeroF of (c₁) is Element of the carrier of (c₁)
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 multF 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 multF of (c₁) . (x,y) is Element of the carrier of (c₁)
[x,y] is set
the multF of (c₁) . [x,y] is set
y * x is Element of the carrier of (c₁)
the multF of (c₁) . (y,x) is Element of the carrier of (c₁)
[y,x] is set
the multF of (c₁) . [y,x] is set
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 multF 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 multF of (c₁) . (x,y) is Element of the carrier of (c₁)
[x,y] is set
the multF 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 multF of (c₁) . ((x * y),a) is Element of the carrier of (c₁)
[(x * y),a] is set
the multF of (c₁) . [(x * y),a] is set
y * a is Element of the carrier of (c₁)
the multF of (c₁) . (y,a) is Element of the carrier of (c₁)
[y,a] is set
the multF of (c₁) . [y,a] is set
x * (y * a) is Element of the carrier of (c₁)
the multF of (c₁) . (x,(y * a)) is Element of the carrier of (c₁)
[x,(y * a)] is set
the multF of (c₁) . [x,(y * a)] is set
the carrier of (c₁) is set
x is Element of the carrier of (c₁)
1. (c₁) is Element of the carrier of (c₁)
the OneF of (c₁) is Element of the carrier of (c₁)
x * (1. (c₁)) is Element of the carrier of (c₁)
the multF 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 multF of (c₁) . (x,(1. (c₁))) is Element of the carrier of (c₁)
[x,(1. (c₁))] is set
the multF of (c₁) . [x,(1. (c₁))] is set
y is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
(c₁) . ((c₁),y) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
[(c₁),y] is set
(c₁) . [(c₁),y] is set
the carrier of (c₁) is set
x is Element of the carrier of (c₁)
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 * (y + a) is Element of the carrier of (c₁)
the multF 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 multF of (c₁) . (x,(y + a)) is Element of the carrier of (c₁)
[x,(y + a)] is set
the multF of (c₁) . [x,(y + a)] is set
x * y is Element of the carrier of (c₁)
the multF of (c₁) . (x,y) is Element of the carrier of (c₁)
[x,y] is set
the multF of (c₁) . [x,y] is set
x * a is Element of the carrier of (c₁)
the multF of (c₁) . (x,a) is Element of the carrier of (c₁)
[x,a] is set
the multF 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
the carrier of (c₁) is set
x is V21() 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 * (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
the carrier of (c₁) is set
x is V21() set
y is V21() set
K110(x,y) is V21() set
a is Element of the carrier of (c₁)
K110(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
[K110(x,y),a] is set
the Mult of (c₁) . [K110(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
x + y is V21() Element of COMPLEX
(x + y) * a is Element of the carrier of (c₁)
[(x + y),a] is set
the Mult of (c₁) . [(x + y),a] is set
the carrier of (c₁) is set
x is V21() set
y is V21() set
K111(x,y) is V21() set
a is Element of the carrier of (c₁)
K111(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
[K111(x,y),a] is set
the Mult of (c₁) . [K111(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 * y is V21() Element of COMPLEX
(x * y) * a is Element of the carrier of (c₁)
[(x * y),a] is set
the Mult of (c₁) . [(x * y),a] is set
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 multF 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 multF of (c₁) . (x,y) is Element of the carrier of (c₁)
[x,y] is set
the multF of (c₁) . [x,y] is set
a is V21() Element of COMPLEX
a * (x * y) 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
[a,(x * y)] is set
the Mult of (c₁) . [a,(x * y)] is set
a * x is Element of the carrier of (c₁)
[a,x] is set
the Mult of (c₁) . [a,x] is set
(a * x) * y is Element of the carrier of (c₁)
the multF of (c₁) . ((a * x),y) is Element of the carrier of (c₁)
[(a * x),y] is set
the multF of (c₁) . [(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 () ()
c₁ is non empty set
(c₁) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital () () ()
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
((Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁),(c₁),(c₁)) is () ()
c₁ is non empty set
(c₁) is non empty strict unital doubleLoopStr
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
doubleLoopStr(# (Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁),(c₁) #) is non empty strict doubleLoopStr
1. (c₁) is Element of the carrier of (c₁)
the carrier of (c₁) is set
the OneF of (c₁) is Element of the carrier of (c₁)
c₁ is non empty set
(c₁) is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative unital associative commutative right-distributive right_unital () () ()
Funcs (c₁,COMPLEX) is non empty FUNCTION_DOMAIN of c₁, COMPLEX
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] is set
[:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like [:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:(Funcs (c₁,COMPLEX)),(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
(c₁) is Relation-like [:COMPLEX,(Funcs (c₁,COMPLEX)):] -defined Funcs (c₁,COMPLEX) -valued Function-like quasi_total Element of bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):]
[:COMPLEX,(Funcs (c₁,COMPLEX)):] is set
[:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
bool [:[:COMPLEX,(Funcs (c₁,COMPLEX)):],(Funcs (c₁,COMPLEX)):] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 1r is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of bool [:c₁,COMPLEX:]
[:c₁,COMPLEX:] is set
bool [:c₁,COMPLEX:] is set
(c₁) is Relation-like c₁ -defined COMPLEX -valued Function-like quasi_total Element of Funcs (c₁,COMPLEX)
c₁ --> 0 is Relation-like c₁ -defined REAL -valued Function-like quasi_total Element of bool [:c₁,REAL:]
[:c₁,REAL:] is set
bool [:c₁,REAL:] is set
((Funcs (c₁,COMPLEX)),(c₁),(c₁),(c₁),(c₁),(c₁)) is () ()
1. (c₁) is right_complementable Element of the carrier of (c₁)
the carrier of (c₁) is set
the OneF of (c₁) is right_complementable Element of the carrier of (c₁)