REAL is non empty V30() V176() V177() V178() V182() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V30() V176() V182() set
omega is non empty epsilon-transitive epsilon-connected ordinal V176() V177() V178() V179() V180() V181() V182() set
bool omega is non empty set
bool NAT is non empty set
[:NAT,REAL:] is non empty V139() V140() V141() set
bool [:NAT,REAL:] is non empty set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V101() ext-real positive non negative V176() V177() V178() V179() V180() V181() V187() Element of NAT
{{},1} is non empty V176() V177() V178() V179() V180() V181() set
RAT is non empty V30() V176() V177() V178() V179() V182() set
INT is non empty V30() V176() V177() V178() V179() V180() V182() set
[:COMPLEX,COMPLEX:] is non empty V139() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V139() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is non empty V139() V140() V141() set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty V139() V140() V141() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is non empty RAT -valued V139() V140() V141() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty RAT -valued V139() V140() V141() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty RAT -valued INT -valued V139() V140() V141() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty RAT -valued INT -valued V139() V140() V141() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty RAT -valued INT -valued V139() V140() V141() V142() set
[:[:NAT,NAT:],NAT:] is non empty RAT -valued INT -valued V139() V140() V141() V142() set
bool [:[:NAT,NAT:],NAT:] is non empty set
K476() is TopStruct
the carrier of K476() is set
[:1,1:] is non empty RAT -valued INT -valued V139() V140() V141() V142() set
bool [:1,1:] is non empty set
[:[:1,1:],1:] is non empty RAT -valued INT -valued V139() V140() V141() V142() set
bool [:[:1,1:],1:] is non empty set
[:[:1,1:],REAL:] is non empty V139() V140() V141() set
bool [:[:1,1:],REAL:] is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V101() ext-real positive non negative V176() V177() V178() V179() V180() V181() V187() Element of NAT
[:2,2:] is non empty RAT -valued INT -valued V139() V140() V141() V142() set
[:[:2,2:],REAL:] is non empty V139() V140() V141() set
bool [:[:2,2:],REAL:] is non empty set
K499() is V217() L20()
K509() is TopSpace-like TopStruct
[:COMPLEX,REAL:] is non empty V139() V140() V141() set
bool [:COMPLEX,REAL:] is non empty set
ExtREAL is non empty V177() set
[:NAT,COMPLEX:] is non empty V139() set
bool [:NAT,COMPLEX:] is non empty set
K694() is non empty set
[:K694(),K694():] is non empty set
[:[:K694(),K694():],K694():] is non empty set
bool [:[:K694(),K694():],K694():] is non empty set
[:COMPLEX,K694():] is non empty set
[:[:COMPLEX,K694():],K694():] is non empty set
bool [:[:COMPLEX,K694():],K694():] is non empty set
K700() is non empty strict CLSStruct
the carrier of K700() is non empty set
bool the carrier of K700() is non empty set
K704() is Element of bool the carrier of K700()
[:K704(),K704():] is set
[:[:K704(),K704():],COMPLEX:] is V139() set
bool [:[:K704(),K704():],COMPLEX:] is non empty set
K712() is Element of bool the carrier of K700()
[:K712(),REAL:] is V139() V140() V141() set
bool [:K712(),REAL:] is non empty set
1r is V11() Element of COMPLEX
|.1r.| is V11() real ext-real non negative Element of REAL
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V101() ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() V187() Element of NAT
- 1r is V11() Element of COMPLEX
X is non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ComplexAlgebraStr
the carrier of X is non empty set
the addF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the multF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[:COMPLEX, the carrier of X:] is non empty set
the Mult of X is non empty Relation-like [:COMPLEX, the carrier of X:] -defined the carrier of X -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of X:], the carrier of X:]
[:[:COMPLEX, the carrier of X:], the carrier of X:] is non empty set
bool [:[:COMPLEX, the carrier of X:], the carrier of X:] is non empty set
1. X is right_complementable Element of the carrier of X
the OneF of X is right_complementable Element of the carrier of X
0. X is V49(X) right_complementable Element of the carrier of X
the ZeroF of X is right_complementable Element of the carrier of X
the addF of X || the carrier of X is Relation-like Function-like set
the addF of X | [: the carrier of X, the carrier of X:] is Relation-like set
the multF of X || the carrier of X is Relation-like Function-like set
the multF of X | [: the carrier of X, the carrier of X:] is Relation-like set
the Mult of X | [:COMPLEX, the carrier of X:] is Relation-like [:COMPLEX, the carrier of X:] -defined the carrier of X -valued Function-like Element of bool [:[:COMPLEX, the carrier of X:], the carrier of X:]
B is non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ComplexAlgebraStr
the carrier of B is non empty set
bool the carrier of B is non empty set
B is non empty set
[:B,B:] is non empty set
[:[:B,B:],B:] is non empty set
bool [:[:B,B:],B:] is non empty set
[:COMPLEX,B:] is non empty set
[:[:COMPLEX,B:],B:] is non empty set
bool [:[:COMPLEX,B:],B:] is non empty set
X1 is non empty Element of bool the carrier of B
f1 is non empty Relation-like [:COMPLEX,B:] -defined B -valued Function-like total quasi_total Element of bool [:[:COMPLEX,B:],B:]
[:COMPLEX, the carrier of B:] is non empty set
the Mult of B is non empty Relation-like [:COMPLEX, the carrier of B:] -defined the carrier of B -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of B:], the carrier of B:]
[:[:COMPLEX, the carrier of B:], the carrier of B:] is non empty set
bool [:[:COMPLEX, the carrier of B:], the carrier of B:] is non empty set
[:COMPLEX,X1:] is non empty set
the Mult of B | [:COMPLEX,X1:] is Relation-like [:COMPLEX, the carrier of B:] -defined the carrier of B -valued Function-like Element of bool [:[:COMPLEX, the carrier of B:], the carrier of B:]
h1 is non empty ComplexAlgebraStr
h is non empty Relation-like [:B,B:] -defined B -valued Function-like total quasi_total Element of bool [:[:B,B:],B:]
g is non empty Relation-like [:B,B:] -defined B -valued Function-like total quasi_total Element of bool [:[:B,B:],B:]
f is Element of B
ONE is Element of B
ComplexAlgebraStr(# B,h,g,f1,f,ONE #) is strict ComplexAlgebraStr
the carrier of h1 is non empty set
g1 is Element of the carrier of h1
F1 is right_complementable Element of the carrier of B
X is V11() set
[X,g1] is set
{X,g1} is non empty set
{X} is non empty V176() set
{{X,g1},{X}} is non empty set
X * g1 is Element of the carrier of h1
the Mult of h1 is non empty Relation-like [:COMPLEX, the carrier of h1:] -defined the carrier of h1 -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of h1:], the carrier of h1:]
[:COMPLEX, the carrier of h1:] is non empty set
[:[:COMPLEX, the carrier of h1:], the carrier of h1:] is non empty set
bool [:[:COMPLEX, the carrier of h1:], the carrier of h1:] is non empty set
the Mult of h1 . [X,g1] is set
X * F1 is right_complementable Element of the carrier of B
[X,F1] is set
{X,F1} is non empty set
{{X,F1},{X}} is non empty set
the Mult of B . [X,F1] is set
X is non empty set
[:X,X:] is non empty set
[:[:X,X:],X:] is non empty set
bool [:[:X,X:],X:] is non empty set
[:COMPLEX,X:] is non empty set
[:[:COMPLEX,X:],X:] is non empty set
bool [:[:COMPLEX,X:],X:] is non empty set
B is non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ComplexAlgebraStr
the carrier of B is non empty set
bool the carrier of B is non empty set
0. B is V49(B) right_complementable Element of the carrier of B
the ZeroF of B is right_complementable Element of the carrier of B
1. B is right_complementable Element of the carrier of B
the OneF of B is right_complementable Element of the carrier of B
the addF of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined the carrier of B -valued Function-like total quasi_total Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]
[: the carrier of B, the carrier of B:] is non empty set
[:[: the carrier of B, the carrier of B:], the carrier of B:] is non empty set
bool [:[: the carrier of B, the carrier of B:], the carrier of B:] is non empty set
the multF of B is non empty Relation-like [: the carrier of B, the carrier of B:] -defined the carrier of B -valued Function-like total quasi_total Element of bool [:[: the carrier of B, the carrier of B:], the carrier of B:]
[:COMPLEX, the carrier of B:] is non empty set
the Mult of B is non empty Relation-like [:COMPLEX, the carrier of B:] -defined the carrier of B -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of B:], the carrier of B:]
[:[:COMPLEX, the carrier of B:], the carrier of B:] is non empty set
bool [:[:COMPLEX, the carrier of B:], the carrier of B:] is non empty set
B is non empty Element of bool the carrier of B
the addF of B || B is Relation-like Function-like set
[:B,B:] is non empty set
the addF of B | [:B,B:] is Relation-like set
the multF of B || B is Relation-like Function-like set
the multF of B | [:B,B:] is Relation-like set
[:COMPLEX,B:] is non empty set
the Mult of B | [:COMPLEX,B:] is Relation-like [:COMPLEX, the carrier of B:] -defined the carrier of B -valued Function-like Element of bool [:[:COMPLEX, the carrier of B:], the carrier of B:]
X1 is Element of X
ONE is Element of X
f is non empty Relation-like [:X,X:] -defined X -valued Function-like total quasi_total Element of bool [:[:X,X:],X:]
g is non empty Relation-like [:X,X:] -defined X -valued Function-like total quasi_total Element of bool [:[:X,X:],X:]
h is non empty Relation-like [:COMPLEX,X:] -defined X -valued Function-like total quasi_total Element of bool [:[:COMPLEX,X:],X:]
ComplexAlgebraStr(# X,g,f,h,ONE,X1 #) is strict ComplexAlgebraStr
f1 is non empty ComplexAlgebraStr
the carrier of f1 is non empty set
h1 is Element of the carrier of f1
g1 is Element of the carrier of f1
h1 + g1 is Element of the carrier of f1
the addF of f1 is non empty Relation-like [: the carrier of f1, the carrier of f1:] -defined the carrier of f1 -valued Function-like total quasi_total Element of bool [:[: the carrier of f1, the carrier of f1:], the carrier of f1:]
[: the carrier of f1, the carrier of f1:] is non empty set
[:[: the carrier of f1, the carrier of f1:], the carrier of f1:] is non empty set
bool [:[: the carrier of f1, the carrier of f1:], the carrier of f1:] is non empty set
the addF of f1 . (h1,g1) is Element of the carrier of f1
[h1,g1] is set
{h1,g1} is non empty set
{h1} is non empty set
{{h1,g1},{h1}} is non empty set
the addF of f1 . [h1,g1] is set
[h1,g1] is Element of [: the carrier of f1, the carrier of f1:]
the addF of B . [h1,g1] is set
the addF of B . (h1,g1) is set
the addF of B . [h1,g1] is set
h1 is Element of the carrier of f1
g1 is Element of the carrier of f1
h1 * g1 is Element of the carrier of f1
the multF of f1 is non empty Relation-like [: the carrier of f1, the carrier of f1:] -defined the carrier of f1 -valued Function-like total quasi_total Element of bool [:[: the carrier of f1, the carrier of f1:], the carrier of f1:]
the multF of f1 . (h1,g1) is Element of the carrier of f1
[h1,g1] is set
{h1,g1} is non empty set
{h1} is non empty set
{{h1,g1},{h1}} is non empty set
the multF of f1 . [h1,g1] is set
[h1,g1] is Element of [: the carrier of f1, the carrier of f1:]
the multF of B . [h1,g1] is set
the multF of B . (h1,g1) is set
the multF of B . [h1,g1] is set
hf1 is Element of the carrier of f1
gf1 is Element of the carrier of f1
hf1 + gf1 is Element of the carrier of f1
the addF of f1 . (hf1,gf1) is Element of the carrier of f1
[hf1,gf1] is set
{hf1,gf1} is non empty set
{hf1} is non empty set
{{hf1,gf1},{hf1}} is non empty set
the addF of f1 . [hf1,gf1] is set
gPh1 is right_complementable Element of the carrier of B
x is right_complementable Element of the carrier of B
gPh1 + x is right_complementable Element of the carrier of B
the addF of B . (gPh1,x) is right_complementable Element of the carrier of B
[gPh1,x] is set
{gPh1,x} is non empty set
{gPh1} is non empty set
{{gPh1,x},{gPh1}} is non empty set
the addF of B . [gPh1,x] is set
gf1 + hf1 is Element of the carrier of f1
the addF of f1 . (gf1,hf1) is Element of the carrier of f1
[gf1,hf1] is set
{gf1,hf1} is non empty set
{gf1} is non empty set
{{gf1,hf1},{gf1}} is non empty set
the addF of f1 . [gf1,hf1] is set
x + gPh1 is right_complementable Element of the carrier of B
the addF of B . (x,gPh1) is right_complementable Element of the carrier of B
[x,gPh1] is set
{x,gPh1} is non empty set
{x} is non empty set
{{x,gPh1},{x}} is non empty set
the addF of B . [x,gPh1] is set
hf1 is Element of the carrier of f1
gf1 is Element of the carrier of f1
gPh1 is Element of the carrier of f1
gf1 + gPh1 is Element of the carrier of f1
the addF of f1 . (gf1,gPh1) is Element of the carrier of f1
[gf1,gPh1] is set
{gf1,gPh1} is non empty set
{gf1} is non empty set
{{gf1,gPh1},{gf1}} is non empty set
the addF of f1 . [gf1,gPh1] is set
hf1 + (gf1 + gPh1) is Element of the carrier of f1
the addF of f1 . (hf1,(gf1 + gPh1)) is Element of the carrier of f1
[hf1,(gf1 + gPh1)] is set
{hf1,(gf1 + gPh1)} is non empty set
{hf1} is non empty set
{{hf1,(gf1 + gPh1)},{hf1}} is non empty set
the addF of f1 . [hf1,(gf1 + gPh1)] is set
x is right_complementable Element of the carrier of B
the addF of B . (x,(gf1 + gPh1)) is set
[x,(gf1 + gPh1)] is set
{x,(gf1 + gPh1)} is non empty set
{x} is non empty set
{{x,(gf1 + gPh1)},{x}} is non empty set
the addF of B . [x,(gf1 + gPh1)] is set
y1 is right_complementable Element of the carrier of B
y1 is right_complementable Element of the carrier of B
y1 + y1 is right_complementable Element of the carrier of B
the addF of B . (y1,y1) is right_complementable Element of the carrier of B
[y1,y1] is set
{y1,y1} is non empty set
{y1} is non empty set
{{y1,y1},{y1}} is non empty set
the addF of B . [y1,y1] is set
x + (y1 + y1) is right_complementable Element of the carrier of B
the addF of B . (x,(y1 + y1)) is right_complementable Element of the carrier of B
[x,(y1 + y1)] is set
{x,(y1 + y1)} is non empty set
{{x,(y1 + y1)},{x}} is non empty set
the addF of B . [x,(y1 + y1)] is set
hf1 + gf1 is Element of the carrier of f1
the addF of f1 . (hf1,gf1) is Element of the carrier of f1
[hf1,gf1] is set
{hf1,gf1} is non empty set
{{hf1,gf1},{hf1}} is non empty set
the addF of f1 . [hf1,gf1] is set
(hf1 + gf1) + gPh1 is Element of the carrier of f1
the addF of f1 . ((hf1 + gf1),gPh1) is Element of the carrier of f1
[(hf1 + gf1),gPh1] is set
{(hf1 + gf1),gPh1} is non empty set
{(hf1 + gf1)} is non empty set
{{(hf1 + gf1),gPh1},{(hf1 + gf1)}} is non empty set
the addF of f1 . [(hf1 + gf1),gPh1] is set
the addF of B . ((hf1 + gf1),y1) is set
[(hf1 + gf1),y1] is set
{(hf1 + gf1),y1} is non empty set
{{(hf1 + gf1),y1},{(hf1 + gf1)}} is non empty set
the addF of B . [(hf1 + gf1),y1] is set
x + y1 is right_complementable Element of the carrier of B
the addF of B . (x,y1) is right_complementable Element of the carrier of B
[x,y1] is set
{x,y1} is non empty set
{{x,y1},{x}} is non empty set
the addF of B . [x,y1] is set
(x + y1) + y1 is right_complementable Element of the carrier of B
the addF of B . ((x + y1),y1) is right_complementable Element of the carrier of B
[(x + y1),y1] is set
{(x + y1),y1} is non empty set
{(x + y1)} is non empty set
{{(x + y1),y1},{(x + y1)}} is non empty set
the addF of B . [(x + y1),y1] is set
hf1 is Element of the carrier of f1
0. f1 is V49(f1) Element of the carrier of f1
the ZeroF of f1 is Element of the carrier of f1
hf1 + (0. f1) is Element of the carrier of f1
the addF of f1 . (hf1,(0. f1)) is Element of the carrier of f1
[hf1,(0. f1)] is set
{hf1,(0. f1)} is non empty set
{hf1} is non empty set
{{hf1,(0. f1)},{hf1}} is non empty set
the addF of f1 . [hf1,(0. f1)] is set
gf1 is right_complementable Element of the carrier of B
gf1 + (0. B) is right_complementable Element of the carrier of B
the addF of B . (gf1,(0. B)) is right_complementable Element of the carrier of B
[gf1,(0. B)] is set
{gf1,(0. B)} is non empty set
{gf1} is non empty set
{{gf1,(0. B)},{gf1}} is non empty set
the addF of B . [gf1,(0. B)] is set
hf1 is Element of the carrier of f1
gf1 is right_complementable Element of the carrier of B
gPh1 is right_complementable Element of the carrier of B
gf1 + gPh1 is right_complementable Element of the carrier of B
the addF of B . (gf1,gPh1) is right_complementable Element of the carrier of B
[gf1,gPh1] is set
{gf1,gPh1} is non empty set
{gf1} is non empty set
{{gf1,gPh1},{gf1}} is non empty set
the addF of B . [gf1,gPh1] is set
- gf1 is right_complementable Element of the carrier of B
x is Element of the carrier of f1
hf1 + x is Element of the carrier of f1
the addF of f1 . (hf1,x) is Element of the carrier of f1
[hf1,x] is set
{hf1,x} is non empty set
{hf1} is non empty set
{{hf1,x},{hf1}} is non empty set
the addF of f1 . [hf1,x] is set
hf1 is Element of the carrier of f1
gf1 is Element of the carrier of f1
hf1 * gf1 is Element of the carrier of f1
the multF of f1 . (hf1,gf1) is Element of the carrier of f1
[hf1,gf1] is set
{hf1,gf1} is non empty set
{hf1} is non empty set
{{hf1,gf1},{hf1}} is non empty set
the multF of f1 . [hf1,gf1] is set
gPh1 is right_complementable Element of the carrier of B
x is right_complementable Element of the carrier of B
gPh1 * x is right_complementable Element of the carrier of B
the multF of B . (gPh1,x) is right_complementable Element of the carrier of B
[gPh1,x] is set
{gPh1,x} is non empty set
{gPh1} is non empty set
{{gPh1,x},{gPh1}} is non empty set
the multF of B . [gPh1,x] is set
gf1 * hf1 is Element of the carrier of f1
the multF of f1 . (gf1,hf1) is Element of the carrier of f1
[gf1,hf1] is set
{gf1,hf1} is non empty set
{gf1} is non empty set
{{gf1,hf1},{gf1}} is non empty set
the multF of f1 . [gf1,hf1] is set
x * gPh1 is right_complementable Element of the carrier of B
the multF of B . (x,gPh1) is right_complementable Element of the carrier of B
[x,gPh1] is set
{x,gPh1} is non empty set
{x} is non empty set
{{x,gPh1},{x}} is non empty set
the multF of B . [x,gPh1] is set
gPh1 is Element of the carrier of f1
hf1 is Element of the carrier of f1
gf1 is Element of the carrier of f1
gf1 * gPh1 is Element of the carrier of f1
the multF of f1 . (gf1,gPh1) is Element of the carrier of f1
[gf1,gPh1] is set
{gf1,gPh1} is non empty set
{gf1} is non empty set
{{gf1,gPh1},{gf1}} is non empty set
the multF of f1 . [gf1,gPh1] is set
hf1 * (gf1 * gPh1) is Element of the carrier of f1
the multF of f1 . (hf1,(gf1 * gPh1)) is Element of the carrier of f1
[hf1,(gf1 * gPh1)] is set
{hf1,(gf1 * gPh1)} is non empty set
{hf1} is non empty set
{{hf1,(gf1 * gPh1)},{hf1}} is non empty set
the multF of f1 . [hf1,(gf1 * gPh1)] is set
the multF of B . (hf1,(gf1 * gPh1)) is set
the multF of B . [hf1,(gf1 * gPh1)] is set
y1 is right_complementable Element of the carrier of B
y1 is right_complementable Element of the carrier of B
x is right_complementable Element of the carrier of B
y1 * x is right_complementable Element of the carrier of B
the multF of B . (y1,x) is right_complementable Element of the carrier of B
[y1,x] is set
{y1,x} is non empty set
{y1} is non empty set
{{y1,x},{y1}} is non empty set
the multF of B . [y1,x] is set
y1 * (y1 * x) is right_complementable Element of the carrier of B
the multF of B . (y1,(y1 * x)) is right_complementable Element of the carrier of B
[y1,(y1 * x)] is set
{y1,(y1 * x)} is non empty set
{y1} is non empty set
{{y1,(y1 * x)},{y1}} is non empty set
the multF of B . [y1,(y1 * x)] is set
hf1 * gf1 is Element of the carrier of f1
the multF of f1 . (hf1,gf1) is Element of the carrier of f1
[hf1,gf1] is set
{hf1,gf1} is non empty set
{{hf1,gf1},{hf1}} is non empty set
the multF of f1 . [hf1,gf1] is set
y1 * y1 is right_complementable Element of the carrier of B
the multF of B . (y1,y1) is right_complementable Element of the carrier of B
[y1,y1] is set
{y1,y1} is non empty set
{{y1,y1},{y1}} is non empty set
the multF of B . [y1,y1] is set
(hf1 * gf1) * gPh1 is Element of the carrier of f1
the multF of f1 . ((hf1 * gf1),gPh1) is Element of the carrier of f1
[(hf1 * gf1),gPh1] is set
{(hf1 * gf1),gPh1} is non empty set
{(hf1 * gf1)} is non empty set
{{(hf1 * gf1),gPh1},{(hf1 * gf1)}} is non empty set
the multF of f1 . [(hf1 * gf1),gPh1] is set
(y1 * y1) * x is right_complementable Element of the carrier of B
the multF of B . ((y1 * y1),x) is right_complementable Element of the carrier of B
[(y1 * y1),x] is set
{(y1 * y1),x} is non empty set
{(y1 * y1)} is non empty set
{{(y1 * y1),x},{(y1 * y1)}} is non empty set
the multF of B . [(y1 * y1),x] is set
hf1 is Element of the carrier of f1
1. f1 is Element of the carrier of f1
the OneF of f1 is Element of the carrier of f1
hf1 * (1. f1) is Element of the carrier of f1
the multF of f1 . (hf1,(1. f1)) is Element of the carrier of f1
[hf1,(1. f1)] is set
{hf1,(1. f1)} is non empty set
{hf1} is non empty set
{{hf1,(1. f1)},{hf1}} is non empty set
the multF of f1 . [hf1,(1. f1)] is set
gf1 is right_complementable Element of the carrier of B
gf1 * (1. B) is right_complementable Element of the carrier of B
the multF of B . (gf1,(1. B)) is right_complementable Element of the carrier of B
[gf1,(1. B)] is set
{gf1,(1. B)} is non empty set
{gf1} is non empty set
{{gf1,(1. B)},{gf1}} is non empty set
the multF of B . [gf1,(1. B)] is set
hf1 is Element of the carrier of f1
gf1 is Element of the carrier of f1
gPh1 is Element of the carrier of f1
gf1 + gPh1 is Element of the carrier of f1
the addF of f1 . (gf1,gPh1) is Element of the carrier of f1
[gf1,gPh1] is set
{gf1,gPh1} is non empty set
{gf1} is non empty set
{{gf1,gPh1},{gf1}} is non empty set
the addF of f1 . [gf1,gPh1] is set
y1 is right_complementable Element of the carrier of B
y1 is right_complementable Element of the carrier of B
y1 + y1 is right_complementable Element of the carrier of B
the addF of B . (y1,y1) is right_complementable Element of the carrier of B
[y1,y1] is set
{y1,y1} is non empty set
{y1} is non empty set
{{y1,y1},{y1}} is non empty set
the addF of B . [y1,y1] is set
hf1 * (gf1 + gPh1) is Element of the carrier of f1
the multF of f1 . (hf1,(gf1 + gPh1)) is Element of the carrier of f1
[hf1,(gf1 + gPh1)] is set
{hf1,(gf1 + gPh1)} is non empty set
{hf1} is non empty set
{{hf1,(gf1 + gPh1)},{hf1}} is non empty set
the multF of f1 . [hf1,(gf1 + gPh1)] is set
x is right_complementable Element of the carrier of B
x * (y1 + y1) is right_complementable Element of the carrier of B
the multF of B . (x,(y1 + y1)) is right_complementable Element of the carrier of B
[x,(y1 + y1)] is set
{x,(y1 + y1)} is non empty set
{x} is non empty set
{{x,(y1 + y1)},{x}} is non empty set
the multF of B . [x,(y1 + y1)] is set
x * y1 is right_complementable Element of the carrier of B
the multF of B . (x,y1) is right_complementable Element of the carrier of B
[x,y1] is set
{x,y1} is non empty set
{{x,y1},{x}} is non empty set
the multF of B . [x,y1] is set
x * y1 is right_complementable Element of the carrier of B
the multF of B . (x,y1) is right_complementable Element of the carrier of B
[x,y1] is set
{x,y1} is non empty set
{{x,y1},{x}} is non empty set
the multF of B . [x,y1] is set
(x * y1) + (x * y1) is right_complementable Element of the carrier of B
the addF of B . ((x * y1),(x * y1)) is right_complementable Element of the carrier of B
[(x * y1),(x * y1)] is set
{(x * y1),(x * y1)} is non empty set
{(x * y1)} is non empty set
{{(x * y1),(x * y1)},{(x * y1)}} is non empty set
the addF of B . [(x * y1),(x * y1)] is set
hf1 * gf1 is Element of the carrier of f1
the multF of f1 . (hf1,gf1) is Element of the carrier of f1
[hf1,gf1] is set
{hf1,gf1} is non empty set
{{hf1,gf1},{hf1}} is non empty set
the multF of f1 . [hf1,gf1] is set
hf1 * gPh1 is Element of the carrier of f1
the multF of f1 . (hf1,gPh1) is Element of the carrier of f1
[hf1,gPh1] is set
{hf1,gPh1} is non empty set
{{hf1,gPh1},{hf1}} is non empty set
the multF of f1 . [hf1,gPh1] is set
(hf1 * gf1) + (hf1 * gPh1) is Element of the carrier of f1
the addF of f1 . ((hf1 * gf1),(hf1 * gPh1)) is Element of the carrier of f1
[(hf1 * gf1),(hf1 * gPh1)] is set
{(hf1 * gf1),(hf1 * gPh1)} is non empty set
{(hf1 * gf1)} is non empty set
{{(hf1 * gf1),(hf1 * gPh1)},{(hf1 * gf1)}} is non empty set
the addF of f1 . [(hf1 * gf1),(hf1 * gPh1)] is set
hf1 is V11() set
gf1 is Element of the carrier of f1
gPh1 is Element of the carrier of f1
gf1 + gPh1 is Element of the carrier of f1
the addF of f1 . (gf1,gPh1) is Element of the carrier of f1
[gf1,gPh1] is set
{gf1,gPh1} is non empty set
{gf1} is non empty set
{{gf1,gPh1},{gf1}} is non empty set
the addF of f1 . [gf1,gPh1] is set
hf1 * (gf1 + gPh1) is Element of the carrier of f1
the Mult of f1 is non empty Relation-like [:COMPLEX, the carrier of f1:] -defined the carrier of f1 -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of f1:], the carrier of f1:]
[:COMPLEX, the carrier of f1:] is non empty set
[:[:COMPLEX, the carrier of f1:], the carrier of f1:] is non empty set
bool [:[:COMPLEX, the carrier of f1:], the carrier of f1:] is non empty set
[hf1,(gf1 + gPh1)] is set
{hf1,(gf1 + gPh1)} is non empty set
{hf1} is non empty V176() set
{{hf1,(gf1 + gPh1)},{hf1}} is non empty set
the Mult of f1 . [hf1,(gf1 + gPh1)] is set
hf1 * gf1 is Element of the carrier of f1
[hf1,gf1] is set
{hf1,gf1} is non empty set
{{hf1,gf1},{hf1}} is non empty set
the Mult of f1 . [hf1,gf1] is set
hf1 * gPh1 is Element of the carrier of f1
[hf1,gPh1] is set
{hf1,gPh1} is non empty set
{{hf1,gPh1},{hf1}} is non empty set
the Mult of f1 . [hf1,gPh1] is set
(hf1 * gf1) + (hf1 * gPh1) is Element of the carrier of f1
the addF of f1 . ((hf1 * gf1),(hf1 * gPh1)) is Element of the carrier of f1
[(hf1 * gf1),(hf1 * gPh1)] is set
{(hf1 * gf1),(hf1 * gPh1)} is non empty set
{(hf1 * gf1)} is non empty set
{{(hf1 * gf1),(hf1 * gPh1)},{(hf1 * gf1)}} is non empty set
the addF of f1 . [(hf1 * gf1),(hf1 * gPh1)] is set
x is right_complementable Element of the carrier of B
hf1 * x is right_complementable Element of the carrier of B
[hf1,x] is set
{hf1,x} is non empty set
{{hf1,x},{hf1}} is non empty set
the Mult of B . [hf1,x] is set
y1 is right_complementable Element of the carrier of B
hf1 * y1 is right_complementable Element of the carrier of B
[hf1,y1] is set
{hf1,y1} is non empty set
{{hf1,y1},{hf1}} is non empty set
the Mult of B . [hf1,y1] is set
x + y1 is right_complementable Element of the carrier of B
the addF of B . (x,y1) is right_complementable Element of the carrier of B
[x,y1] is set
{x,y1} is non empty set
{x} is non empty set
{{x,y1},{x}} is non empty set
the addF of B . [x,y1] is set
hf1 * (x + y1) is right_complementable Element of the carrier of B
[hf1,(x + y1)] is set
{hf1,(x + y1)} is non empty set
{{hf1,(x + y1)},{hf1}} is non empty set
the Mult of B . [hf1,(x + y1)] is set
(hf1 * x) + (hf1 * y1) is right_complementable Element of the carrier of B
the addF of B . ((hf1 * x),(hf1 * y1)) is right_complementable Element of the carrier of B
[(hf1 * x),(hf1 * y1)] is set
{(hf1 * x),(hf1 * y1)} is non empty set
{(hf1 * x)} is non empty set
{{(hf1 * x),(hf1 * y1)},{(hf1 * x)}} is non empty set
the addF of B . [(hf1 * x),(hf1 * y1)] is set
hf1 is V11() set
gf1 is V11() set
hf1 + gf1 is V11() Element of COMPLEX
gPh1 is Element of the carrier of f1
(hf1 + gf1) * gPh1 is Element of the carrier of f1
the Mult of f1 is non empty Relation-like [:COMPLEX, the carrier of f1:] -defined the carrier of f1 -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of f1:], the carrier of f1:]
[:COMPLEX, the carrier of f1:] is non empty set
[:[:COMPLEX, the carrier of f1:], the carrier of f1:] is non empty set
bool [:[:COMPLEX, the carrier of f1:], the carrier of f1:] is non empty set
[(hf1 + gf1),gPh1] is set
{(hf1 + gf1),gPh1} is non empty set
{(hf1 + gf1)} is non empty V176() set
{{(hf1 + gf1),gPh1},{(hf1 + gf1)}} is non empty set
the Mult of f1 . [(hf1 + gf1),gPh1] is set
hf1 * gPh1 is Element of the carrier of f1
[hf1,gPh1] is set
{hf1,gPh1} is non empty set
{hf1} is non empty V176() set
{{hf1,gPh1},{hf1}} is non empty set
the Mult of f1 . [hf1,gPh1] is set
gf1 * gPh1 is Element of the carrier of f1
[gf1,gPh1] is set
{gf1,gPh1} is non empty set
{gf1} is non empty V176() set
{{gf1,gPh1},{gf1}} is non empty set
the Mult of f1 . [gf1,gPh1] is set
(hf1 * gPh1) + (gf1 * gPh1) is Element of the carrier of f1
the addF of f1 . ((hf1 * gPh1),(gf1 * gPh1)) is Element of the carrier of f1
[(hf1 * gPh1),(gf1 * gPh1)] is set
{(hf1 * gPh1),(gf1 * gPh1)} is non empty set
{(hf1 * gPh1)} is non empty set
{{(hf1 * gPh1),(gf1 * gPh1)},{(hf1 * gPh1)}} is non empty set
the addF of f1 . [(hf1 * gPh1),(gf1 * gPh1)] is set
x is right_complementable Element of the carrier of B
hf1 * x is right_complementable Element of the carrier of B
[hf1,x] is set
{hf1,x} is non empty set
{{hf1,x},{hf1}} is non empty set
the Mult of B . [hf1,x] is set
gf1 * x is right_complementable Element of the carrier of B
[gf1,x] is set
{gf1,x} is non empty set
{{gf1,x},{gf1}} is non empty set
the Mult of B . [gf1,x] is set
(hf1 + gf1) * x is right_complementable Element of the carrier of B
[(hf1 + gf1),x] is set
{(hf1 + gf1),x} is non empty set
{{(hf1 + gf1),x},{(hf1 + gf1)}} is non empty set
the Mult of B . [(hf1 + gf1),x] is set
(hf1 * x) + (gf1 * x) is right_complementable Element of the carrier of B
the addF of B . ((hf1 * x),(gf1 * x)) is right_complementable Element of the carrier of B
[(hf1 * x),(gf1 * x)] is set
{(hf1 * x),(gf1 * x)} is non empty set
{(hf1 * x)} is non empty set
{{(hf1 * x),(gf1 * x)},{(hf1 * x)}} is non empty set
the addF of B . [(hf1 * x),(gf1 * x)] is set
hf1 is V11() set
gf1 is V11() set
hf1 * gf1 is V11() Element of COMPLEX
gPh1 is Element of the carrier of f1
(hf1 * gf1) * gPh1 is Element of the carrier of f1
the Mult of f1 is non empty Relation-like [:COMPLEX, the carrier of f1:] -defined the carrier of f1 -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of f1:], the carrier of f1:]
[:COMPLEX, the carrier of f1:] is non empty set
[:[:COMPLEX, the carrier of f1:], the carrier of f1:] is non empty set
bool [:[:COMPLEX, the carrier of f1:], the carrier of f1:] is non empty set
[(hf1 * gf1),gPh1] is set
{(hf1 * gf1),gPh1} is non empty set
{(hf1 * gf1)} is non empty V176() set
{{(hf1 * gf1),gPh1},{(hf1 * gf1)}} is non empty set
the Mult of f1 . [(hf1 * gf1),gPh1] is set
gf1 * gPh1 is Element of the carrier of f1
[gf1,gPh1] is set
{gf1,gPh1} is non empty set
{gf1} is non empty V176() set
{{gf1,gPh1},{gf1}} is non empty set
the Mult of f1 . [gf1,gPh1] is set
hf1 * (gf1 * gPh1) is Element of the carrier of f1
[hf1,(gf1 * gPh1)] is set
{hf1,(gf1 * gPh1)} is non empty set
{hf1} is non empty V176() set
{{hf1,(gf1 * gPh1)},{hf1}} is non empty set
the Mult of f1 . [hf1,(gf1 * gPh1)] is set
x is right_complementable Element of the carrier of B
gf1 * x is right_complementable Element of the carrier of B
[gf1,x] is set
{gf1,x} is non empty set
{{gf1,x},{gf1}} is non empty set
the Mult of B . [gf1,x] is set
hf1 * (gf1 * x) is right_complementable Element of the carrier of B
[hf1,(gf1 * x)] is set
{hf1,(gf1 * x)} is non empty set
{{hf1,(gf1 * x)},{hf1}} is non empty set
the Mult of B . [hf1,(gf1 * x)] is set
(hf1 * gf1) * x is right_complementable Element of the carrier of B
[(hf1 * gf1),x] is set
{(hf1 * gf1),x} is non empty set
{{(hf1 * gf1),x},{(hf1 * gf1)}} is non empty set
the Mult of B . [(hf1 * gf1),x] is set
hf1 is Element of the carrier of f1
gf1 is Element of the carrier of f1
hf1 * gf1 is Element of the carrier of f1
the multF of f1 . (hf1,gf1) is Element of the carrier of f1
[hf1,gf1] is set
{hf1,gf1} is non empty set
{hf1} is non empty set
{{hf1,gf1},{hf1}} is non empty set
the multF of f1 . [hf1,gf1] is set
gPh1 is V11() Element of COMPLEX
gPh1 * (hf1 * gf1) is Element of the carrier of f1
the Mult of f1 is non empty Relation-like [:COMPLEX, the carrier of f1:] -defined the carrier of f1 -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of f1:], the carrier of f1:]
[:COMPLEX, the carrier of f1:] is non empty set
[:[:COMPLEX, the carrier of f1:], the carrier of f1:] is non empty set
bool [:[:COMPLEX, the carrier of f1:], the carrier of f1:] is non empty set
[gPh1,(hf1 * gf1)] is set
{gPh1,(hf1 * gf1)} is non empty set
{gPh1} is non empty V176() set
{{gPh1,(hf1 * gf1)},{gPh1}} is non empty set
the Mult of f1 . [gPh1,(hf1 * gf1)] is set
gPh1 * hf1 is Element of the carrier of f1
[gPh1,hf1] is set
{gPh1,hf1} is non empty set
{{gPh1,hf1},{gPh1}} is non empty set
the Mult of f1 . [gPh1,hf1] is set
(gPh1 * hf1) * gf1 is Element of the carrier of f1
the multF of f1 . ((gPh1 * hf1),gf1) is Element of the carrier of f1
[(gPh1 * hf1),gf1] is set
{(gPh1 * hf1),gf1} is non empty set
{(gPh1 * hf1)} is non empty set
{{(gPh1 * hf1),gf1},{(gPh1 * hf1)}} is non empty set
the multF of f1 . [(gPh1 * hf1),gf1] is set
x is right_complementable Element of the carrier of B
gPh1 * x is right_complementable Element of the carrier of B
[gPh1,x] is set
{gPh1,x} is non empty set
{{gPh1,x},{gPh1}} is non empty set
the Mult of B . [gPh1,x] is set
y1 is right_complementable Element of the carrier of B
x * y1 is right_complementable Element of the carrier of B
the multF of B . (x,y1) is right_complementable Element of the carrier of B
[x,y1] is set
{x,y1} is non empty set
{x} is non empty set
{{x,y1},{x}} is non empty set
the multF of B . [x,y1] is set
gPh1 * (x * y1) is right_complementable Element of the carrier of B
[gPh1,(x * y1)] is set
{gPh1,(x * y1)} is non empty set
{{gPh1,(x * y1)},{gPh1}} is non empty set
the Mult of B . [gPh1,(x * y1)] is set
(gPh1 * x) * y1 is right_complementable Element of the carrier of B
the multF of B . ((gPh1 * x),y1) is right_complementable Element of the carrier of B
[(gPh1 * x),y1] is set
{(gPh1 * x),y1} is non empty set
{(gPh1 * x)} is non empty set
{{(gPh1 * x),y1},{(gPh1 * x)}} is non empty set
the multF of B . [(gPh1 * x),y1] is set
0. f1 is V49(f1) Element of the carrier of f1
the ZeroF of f1 is Element of the carrier of f1
1. f1 is Element of the carrier of f1
the OneF of f1 is Element of the carrier of f1
X is non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ComplexAlgebraStr
[#] X is non empty non proper add-closed having-inverse additively-closed Element of bool the carrier of X
the carrier of X is non empty set
bool the carrier of X is non empty set
[:COMPLEX, the carrier of X:] is non empty set
the Mult of X is non empty Relation-like [:COMPLEX, the carrier of X:] -defined the carrier of X -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of X:], the carrier of X:]
[:[:COMPLEX, the carrier of X:], the carrier of X:] is non empty set
bool [:[:COMPLEX, the carrier of X:], the carrier of X:] is non empty set
[:COMPLEX,([#] X):] is non empty set
the Mult of X | [:COMPLEX,([#] X):] is Relation-like [:COMPLEX, the carrier of X:] -defined the carrier of X -valued Function-like Element of bool [:[:COMPLEX, the carrier of X:], the carrier of X:]
the addF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
[: the carrier of X, the carrier of X:] is non empty set
[:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
bool [:[: the carrier of X, the carrier of X:], the carrier of X:] is non empty set
the addF of X || ([#] X) is Relation-like Function-like set
[:([#] X),([#] X):] is non empty set
the addF of X | [:([#] X),([#] X):] is Relation-like set
the multF of X is non empty Relation-like [: the carrier of X, the carrier of X:] -defined the carrier of X -valued Function-like total quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]
the multF of X || ([#] X) is Relation-like Function-like set
the multF of X | [:([#] X),([#] X):] is Relation-like set
1. X is right_complementable Element of the carrier of X
the OneF of X is right_complementable Element of the carrier of X
0. X is V49(X) right_complementable Element of the carrier of X
the ZeroF of X is right_complementable Element of the carrier of X
ComplexAlgebraStr(# the carrier of X, the multF of X, the addF of X, the Mult of X,(1. X),(0. X) #) is strict ComplexAlgebraStr
X is non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ComplexAlgebraStr
the carrier of X is non empty set
bool the carrier of X is non empty set
X is non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative vector-associative ComplexAlgebraStr
the carrier of X is non empty set
bool the carrier of X is non empty set
B is Element of bool the carrier of X
[:COMPLEX, the carrier of X:] is non empty set
the Mult of X is non empty Relation-like [:COMPLEX, the carrier of X:] -defined the carrier of X -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of X:], the carrier of X:]
[:[:COMPLEX, the carrier of X:], the carrier of X:] is non empty set
bool [:[:COMPLEX, the carrier of X:], the carrier of X:] is non empty set
[:COMPLEX,B:] is set
the Mult of X | [:COMPLEX,B:] is Relation-like [:COMPLEX, the carrier of X:] -defined the carrier of X -valued Function-like Element of bool [:[:COMPLEX, the carrier of X:], the carrier of X:]
[:[:COMPLEX,B:],B:] is set
bool [:[:COMPLEX,B:],B:] is non empty set
dom the Mult of X is Relation-like COMPLEX -defined the carrier of X -valued Element of bool [:COMPLEX, the carrier of X:]
bool [:COMPLEX, the carrier of X:] is non empty set
B is set
( the Mult of X | [:COMPLEX,B:]) . B is set
X1 is set
ONE is set
[X1,ONE] is set
{X1,ONE} is non empty set
{X1} is non empty set
{{X1,ONE},{X1}} is non empty set
f is V11() set
[f,ONE] is set
{f,ONE} is non empty set
{f} is non empty V176() set
{{f,ONE},{f}} is non empty set
dom ( the Mult of X | [:COMPLEX,B:]) is Relation-like COMPLEX -defined the carrier of X -valued Element of bool [:COMPLEX, the carrier of X:]
g is right_complementable Element of the carrier of X
f * g is right_complementable Element of the carrier of X
[f,g] is set
{f,g} is non empty set
{{f,g},{f}} is non empty set
the Mult of X . [f,g] is set
dom ( the Mult of X | [:COMPLEX,B:]) is Relation-like COMPLEX -defined the carrier of X -valued Element of bool [:COMPLEX, the carrier of X:]
X is non empty set
[:X,COMPLEX:] is non empty V139() set
bool [:X,COMPLEX:] is non empty set
{ b1 where b1 is non empty Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [:X,COMPLEX:] : b1 | X is bounded } is set
CAlgebra X is non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative strict vector-associative ComplexAlgebraStr
Funcs (X,COMPLEX) is non empty functional FUNCTION_DOMAIN of X, COMPLEX
ComplexFuncMult X is non empty Relation-like [:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):] -defined Funcs (X,COMPLEX) -valued Function-like total quasi_total Function-yielding V160() Element of bool [:[:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):]
[:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):] is non empty set
[:[:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):] is non empty set
bool [:[:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):] is non empty set
ComplexFuncAdd X is non empty Relation-like [:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):] -defined Funcs (X,COMPLEX) -valued Function-like total quasi_total Function-yielding V160() Element of bool [:[:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):]
ComplexFuncExtMult X is non empty Relation-like [:COMPLEX,(Funcs (X,COMPLEX)):] -defined Funcs (X,COMPLEX) -valued Function-like total quasi_total Function-yielding V160() Element of bool [:[:COMPLEX,(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):]
[:COMPLEX,(Funcs (X,COMPLEX)):] is non empty set
[:[:COMPLEX,(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):] is non empty set
bool [:[:COMPLEX,(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):] is non empty set
ComplexFuncUnit X is Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs (X,COMPLEX)
X --> 1r is non empty Relation-like X -defined COMPLEX -valued Function-like constant total quasi_total V139() Element of bool [:X,COMPLEX:]
ComplexFuncZero X is Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs (X,COMPLEX)
X --> 0 is non empty Relation-like X -defined REAL -valued NAT -valued RAT -valued INT -valued Function-like constant total quasi_total V139() V140() V141() V142() bounded_above bounded_below bounded Element of bool [:X,REAL:]
[:X,REAL:] is non empty V139() V140() V141() set
bool [:X,REAL:] is non empty set
ComplexAlgebraStr(# (Funcs (X,COMPLEX)),(ComplexFuncMult X),(ComplexFuncAdd X),(ComplexFuncExtMult X),(ComplexFuncUnit X),(ComplexFuncZero X) #) is strict ComplexAlgebraStr
the carrier of (CAlgebra X) is non empty set
bool the carrier of (CAlgebra X) is non empty set
B is set
B is non empty Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [:X,COMPLEX:]
B | X is Relation-like X -defined COMPLEX -valued Function-like V139() Element of bool [:X,COMPLEX:]
0c is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative V176() V177() V178() V179() V180() V181() V182() Element of COMPLEX
X --> 0c is non empty Relation-like X -defined COMPLEX -valued RAT -valued Function-like constant total quasi_total V139() V140() V141() V142() bounded_above bounded_below bounded Element of bool [:X,COMPLEX:]
B is non empty Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [:X,COMPLEX:]
B | X is Relation-like X -defined COMPLEX -valued Function-like V139() Element of bool [:X,COMPLEX:]
X is non empty set
CAlgebra X is non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative strict vector-associative ComplexAlgebraStr
Funcs (X,COMPLEX) is non empty functional FUNCTION_DOMAIN of X, COMPLEX
ComplexFuncMult X is non empty Relation-like [:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):] -defined Funcs (X,COMPLEX) -valued Function-like total quasi_total Function-yielding V160() Element of bool [:[:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):]
[:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):] is non empty set
[:[:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):] is non empty set
bool [:[:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):] is non empty set
ComplexFuncAdd X is non empty Relation-like [:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):] -defined Funcs (X,COMPLEX) -valued Function-like total quasi_total Function-yielding V160() Element of bool [:[:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):]
ComplexFuncExtMult X is non empty Relation-like [:COMPLEX,(Funcs (X,COMPLEX)):] -defined Funcs (X,COMPLEX) -valued Function-like total quasi_total Function-yielding V160() Element of bool [:[:COMPLEX,(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):]
[:COMPLEX,(Funcs (X,COMPLEX)):] is non empty set
[:[:COMPLEX,(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):] is non empty set
bool [:[:COMPLEX,(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):] is non empty set
ComplexFuncUnit X is Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs (X,COMPLEX)
X --> 1r is non empty Relation-like X -defined COMPLEX -valued Function-like constant total quasi_total V139() Element of bool [:X,COMPLEX:]
[:X,COMPLEX:] is non empty V139() set
bool [:X,COMPLEX:] is non empty set
ComplexFuncZero X is Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs (X,COMPLEX)
X --> 0 is non empty Relation-like X -defined REAL -valued NAT -valued RAT -valued INT -valued Function-like constant total quasi_total V139() V140() V141() V142() bounded_above bounded_below bounded Element of bool [:X,REAL:]
[:X,REAL:] is non empty V139() V140() V141() set
bool [:X,REAL:] is non empty set
ComplexAlgebraStr(# (Funcs (X,COMPLEX)),(ComplexFuncMult X),(ComplexFuncAdd X),(ComplexFuncExtMult X),(ComplexFuncUnit X),(ComplexFuncZero X) #) is strict ComplexAlgebraStr
the carrier of (CAlgebra X) is non empty set
B is right_complementable Element of the carrier of (CAlgebra X)
1r * B is right_complementable Element of the carrier of (CAlgebra X)
the Mult of (CAlgebra X) is non empty Relation-like [:COMPLEX, the carrier of (CAlgebra X):] -defined the carrier of (CAlgebra X) -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of (CAlgebra X):], the carrier of (CAlgebra X):]
[:COMPLEX, the carrier of (CAlgebra X):] is non empty set
[:[:COMPLEX, the carrier of (CAlgebra X):], the carrier of (CAlgebra X):] is non empty set
bool [:[:COMPLEX, the carrier of (CAlgebra X):], the carrier of (CAlgebra X):] is non empty set
[1r,B] is set
{1r,B} is non empty set
{1r} is non empty V176() set
{{1r,B},{1r}} is non empty set
the Mult of (CAlgebra X) . [1r,B] is set
X is non empty set
CAlgebra X is non empty right_complementable Abelian add-associative right_zeroed unital associative commutative right-distributive right_unital well-unital left_unital vector-distributive scalar-distributive scalar-associative scalar-unital strict vector-associative ComplexAlgebraStr
Funcs (X,COMPLEX) is non empty functional FUNCTION_DOMAIN of X, COMPLEX
ComplexFuncMult X is non empty Relation-like [:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):] -defined Funcs (X,COMPLEX) -valued Function-like total quasi_total Function-yielding V160() Element of bool [:[:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):]
[:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):] is non empty set
[:[:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):] is non empty set
bool [:[:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):] is non empty set
ComplexFuncAdd X is non empty Relation-like [:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):] -defined Funcs (X,COMPLEX) -valued Function-like total quasi_total Function-yielding V160() Element of bool [:[:(Funcs (X,COMPLEX)),(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):]
ComplexFuncExtMult X is non empty Relation-like [:COMPLEX,(Funcs (X,COMPLEX)):] -defined Funcs (X,COMPLEX) -valued Function-like total quasi_total Function-yielding V160() Element of bool [:[:COMPLEX,(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):]
[:COMPLEX,(Funcs (X,COMPLEX)):] is non empty set
[:[:COMPLEX,(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):] is non empty set
bool [:[:COMPLEX,(Funcs (X,COMPLEX)):],(Funcs (X,COMPLEX)):] is non empty set
ComplexFuncUnit X is Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs (X,COMPLEX)
X --> 1r is non empty Relation-like X -defined COMPLEX -valued Function-like constant total quasi_total V139() Element of bool [:X,COMPLEX:]
[:X,COMPLEX:] is non empty V139() set
bool [:X,COMPLEX:] is non empty set
ComplexFuncZero X is Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs (X,COMPLEX)
X --> 0 is non empty Relation-like X -defined REAL -valued NAT -valued RAT -valued INT -valued Function-like constant total quasi_total V139() V140() V141() V142() bounded_above bounded_below bounded Element of bool [:X,REAL:]
[:X,REAL:] is non empty V139() V140() V141() set
bool [:X,REAL:] is non empty set
ComplexAlgebraStr(# (Funcs (X,COMPLEX)),(ComplexFuncMult X),(ComplexFuncAdd X),(ComplexFuncExtMult X),(ComplexFuncUnit X),(ComplexFuncZero X) #) is strict ComplexAlgebraStr
(X) is non empty Element of bool the carrier of (CAlgebra X)
the carrier of (CAlgebra X) is non empty set
bool the carrier of (CAlgebra X) is non empty set
{ b1 where b1 is non empty Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [:X,COMPLEX:] : b1 | X is bounded } is set
X1 is right_complementable Element of the carrier of (CAlgebra X)
ONE is right_complementable Element of the carrier of (CAlgebra X)
X1 + ONE is right_complementable Element of the carrier of (CAlgebra X)
the addF of (CAlgebra X) is non empty Relation-like [: the carrier of (CAlgebra X), the carrier of (CAlgebra X):] -defined the carrier of (CAlgebra X) -valued Function-like total quasi_total Element of bool [:[: the carrier of (CAlgebra X), the carrier of (CAlgebra X):], the carrier of (CAlgebra X):]
[: the carrier of (CAlgebra X), the carrier of (CAlgebra X):] is non empty set
[:[: the carrier of (CAlgebra X), the carrier of (CAlgebra X):], the carrier of (CAlgebra X):] is non empty set
bool [:[: the carrier of (CAlgebra X), the carrier of (CAlgebra X):], the carrier of (CAlgebra X):] is non empty set
the addF of (CAlgebra X) . (X1,ONE) is right_complementable Element of the carrier of (CAlgebra X)
[X1,ONE] is set
{X1,ONE} is non empty set
{X1} is non empty set
{{X1,ONE},{X1}} is non empty set
the addF of (CAlgebra X) . [X1,ONE] is set
f is non empty Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [:X,COMPLEX:]
f | X is Relation-like X -defined COMPLEX -valued Function-like V139() Element of bool [:X,COMPLEX:]
g is non empty Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [:X,COMPLEX:]
g | X is Relation-like X -defined COMPLEX -valued Function-like V139() Element of bool [:X,COMPLEX:]
f + g is non empty Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [:X,COMPLEX:]
dom (f + g) is Element of bool X
bool X is non empty set
X /\ X is set
(f + g) | X is Relation-like X -defined COMPLEX -valued Function-like V139() Element of bool [:X,COMPLEX:]
h is Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs (X,COMPLEX)
dom f is Element of bool X
dom g is Element of bool X
(dom f) /\ (dom g) is Element of bool X
X /\ (dom g) is Element of bool X
dom h is Element of bool X
f1 is set
h . f1 is V11() set
f . f1 is V11() set
g . f1 is V11() set
(f . f1) + (g . f1) is V11() Element of COMPLEX
f1 is Relation-like Function-like set
dom f1 is set
rng f1 is set
X1 is right_complementable Element of the carrier of (CAlgebra X)
- X1 is right_complementable Element of the carrier of (CAlgebra X)
ONE is non empty Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [:X,COMPLEX:]
ONE | X is Relation-like X -defined COMPLEX -valued Function-like V139() Element of bool [:X,COMPLEX:]
- ONE is non empty Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [:X,COMPLEX:]
K38(1) is non empty V11() real ext-real non positive negative set
K38(1) (#) ONE is Relation-like X -defined Function-like total V139() set
(- ONE) | X is Relation-like X -defined COMPLEX -valued Function-like V139() Element of bool [:X,COMPLEX:]
f is Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs (X,COMPLEX)
- 1r is V11() Element of COMPLEX
(- 1r) * X1 is right_complementable Element of the carrier of (CAlgebra X)
the Mult of (CAlgebra X) is non empty Relation-like [:COMPLEX, the carrier of (CAlgebra X):] -defined the carrier of (CAlgebra X) -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of (CAlgebra X):], the carrier of (CAlgebra X):]
[:COMPLEX, the carrier of (CAlgebra X):] is non empty set
[:[:COMPLEX, the carrier of (CAlgebra X):], the carrier of (CAlgebra X):] is non empty set
bool [:[:COMPLEX, the carrier of (CAlgebra X):], the carrier of (CAlgebra X):] is non empty set
[(- 1r),X1] is set
{(- 1r),X1} is non empty set
{(- 1r)} is non empty V176() set
{{(- 1r),X1},{(- 1r)}} is non empty set
the Mult of (CAlgebra X) . [(- 1r),X1] is set
dom ONE is Element of bool X
bool X is non empty set
h is set
dom f is Element of bool X
f . h is V11() set
g is Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs (X,COMPLEX)
f1 is Element of X
g . f1 is V11() Element of COMPLEX
(- 1r) * (g . f1) is V11() Element of COMPLEX
ONE . h is V11() set
- (ONE . h) is V11() Element of COMPLEX
h is Relation-like Function-like set
dom h is set
rng h is set
X1 is V11() set
ONE is right_complementable Element of the carrier of (CAlgebra X)
X1 * ONE is right_complementable Element of the carrier of (CAlgebra X)
the Mult of (CAlgebra X) is non empty Relation-like [:COMPLEX, the carrier of (CAlgebra X):] -defined the carrier of (CAlgebra X) -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of (CAlgebra X):], the carrier of (CAlgebra X):]
[:COMPLEX, the carrier of (CAlgebra X):] is non empty set
[:[:COMPLEX, the carrier of (CAlgebra X):], the carrier of (CAlgebra X):] is non empty set
bool [:[:COMPLEX, the carrier of (CAlgebra X):], the carrier of (CAlgebra X):] is non empty set
[X1,ONE] is set
{X1,ONE} is non empty set
{X1} is non empty V176() set
{{X1,ONE},{X1}} is non empty set
the Mult of (CAlgebra X) . [X1,ONE] is set
f is non empty Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [:X,COMPLEX:]
f | X is Relation-like X -defined COMPLEX -valued Function-like V139() Element of bool [:X,COMPLEX:]
X1 (#) f is non empty Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of bool [:X,COMPLEX:]
(X1 (#) f) | X is Relation-like X -defined COMPLEX -valued Function-like V139() Element of bool [:X,COMPLEX:]
g is Relation-like X -defined COMPLEX -valued Function-like total quasi_total V139() Element of Funcs (X,COMPLEX)
dom f is