:: CC0SP1 semantic presentation

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

{ b

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

{ b

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