:: 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