:: C0SP1 semantic presentation

REAL is non empty V30() V177() V178() V179() V183() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V177() V178() V179() V180() V181() V182() V183() Element of bool REAL

bool REAL is non empty set

omega is non empty epsilon-transitive epsilon-connected ordinal V177() V178() V179() V180() V181() V182() V183() set

bool omega is non empty set

bool NAT is non empty set

[:NAT,REAL:] is non empty V150() V151() V152() set

bool [:NAT,REAL:] is non empty set

K207() is non empty set

[:K207(),K207():] is non empty set

[:[:K207(),K207():],K207():] is non empty set

bool [:[:K207(),K207():],K207():] is non empty set

[:REAL,K207():] is non empty set

[:[:REAL,K207():],K207():] is non empty set

bool [:[:REAL,K207():],K207():] is non empty set

K213() is RLSStruct

the carrier of K213() is set

bool the carrier of K213() is non empty set

K217() is Element of bool the carrier of K213()

[:K217(),K217():] is set

[:[:K217(),K217():],REAL:] is V150() V151() V152() set

bool [:[:K217(),K217():],REAL:] is non empty set

the_set_of_l1RealSequences is Element of bool the carrier of K213()

[:the_set_of_l1RealSequences,REAL:] is V150() V151() V152() set

bool [:the_set_of_l1RealSequences,REAL:] is non empty set

COMPLEX is non empty V30() V177() V183() set

RAT is non empty V30() V177() V178() V179() V180() V183() set

INT is non empty V30() V177() V178() V179() V180() V181() V183() set

[:COMPLEX,COMPLEX:] is non empty V150() set

bool [:COMPLEX,COMPLEX:] is non empty set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V150() set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

[:REAL,REAL:] is non empty V150() V151() V152() set

bool [:REAL,REAL:] is non empty set

[:[:REAL,REAL:],REAL:] is non empty V150() V151() V152() set

bool [:[:REAL,REAL:],REAL:] is non empty set

[:RAT,RAT:] is non empty RAT -valued V150() V151() V152() set

bool [:RAT,RAT:] is non empty set

[:[:RAT,RAT:],RAT:] is non empty RAT -valued V150() V151() V152() set

bool [:[:RAT,RAT:],RAT:] is non empty set

[:INT,INT:] is non empty RAT -valued INT -valued V150() V151() V152() set

bool [:INT,INT:] is non empty set

[:[:INT,INT:],INT:] is non empty RAT -valued INT -valued V150() V151() V152() set

bool [:[:INT,INT:],INT:] is non empty set

[:NAT,NAT:] is non empty RAT -valued INT -valued V150() V151() V152() V153() set

[:[:NAT,NAT:],NAT:] is non empty RAT -valued INT -valued V150() V151() V152() V153() set

bool [:[:NAT,NAT:],NAT:] is non empty set

[:COMPLEX,REAL:] is non empty V150() V151() V152() set

bool [:COMPLEX,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 V177() V178() V179() V180() V181() V182() V183() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V111() V112() ext-real positive non negative V177() V178() V179() V180() V181() V182() Element of NAT

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V111() V112() ext-real non positive non negative V177() V178() V179() V180() V181() V182() V183() Element of NAT

1r is V11() Element of COMPLEX

|.1r.| is V11() real ext-real Element of REAL

2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real V111() V112() ext-real positive non negative V177() V178() V179() V180() V181() V182() Element of NAT

- 1 is V11() real ext-real non positive Element of REAL

X is non empty addLoopStr

the carrier of X is non empty set

bool the carrier of X is non empty set

X is non empty addLoopStr

the carrier of X is non empty set

bool the carrier of X is non empty set

X is non empty addLoopStr

[#] X is non empty non proper Element of bool the carrier of X

the carrier of X is non empty set

bool the carrier of X is non empty set

B is Element of the carrier of X

B is Element of the carrier of X

B + B is Element of 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 V23([: the carrier of X, the carrier of X:]) 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 . (B,B) is Element of the carrier of X

[B,B] is set

{B,B} is non empty set

{B} is non empty set

{{B,B},{B}} is non empty set

the addF of X . [B,B] is set

X is non empty addLoopStr

[#] X is non empty non proper Element of bool the carrier of X

the carrier of X is non empty set

bool the carrier of X is non empty set

B is Element of the carrier of X

- B is Element of the carrier of X

X is non empty addLoopStr

[#] X is non empty non proper Element of bool the carrier of X

the carrier of X is non empty set

bool the carrier of X is non empty set

X is non empty doubleLoopStr

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

B is Element of bool the carrier of X

X is non empty addLoopStr

the carrier of X is non empty set

bool the carrier of X is non empty set

[#] X is non empty non proper add-closed (X) Element of bool the carrier of X

X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

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 V23([: the carrier of X, the carrier of X:]) 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 V23([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

1. X is left_complementable right_complementable complementable Element of the carrier of X

the OneF of X is left_complementable right_complementable complementable Element of the carrier of X

0. X is V49(X) left_complementable right_complementable complementable Element of the carrier of X

the ZeroF of X is left_complementable right_complementable 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

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

B is Element of X

B is Element of X

ONE is non empty Relation-like [:X,X:] -defined X -valued Function-like V23([:X,X:]) quasi_total Element of bool [:[:X,X:],X:]

f is non empty Relation-like [:X,X:] -defined X -valued Function-like V23([:X,X:]) quasi_total Element of bool [:[:X,X:],X:]

doubleLoopStr(# X,ONE,f,B,B #) is non empty strict doubleLoopStr

g is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

the carrier of g is non empty set

bool the carrier of g is non empty set

the addF of g is non empty Relation-like [: the carrier of g, the carrier of g:] -defined the carrier of g -valued Function-like V23([: the carrier of g, the carrier of g:]) quasi_total Element of bool [:[: the carrier of g, the carrier of g:], the carrier of g:]

[: the carrier of g, the carrier of g:] is non empty set

[:[: the carrier of g, the carrier of g:], the carrier of g:] is non empty set

bool [:[: the carrier of g, the carrier of g:], the carrier of g:] is non empty set

the multF of g is non empty Relation-like [: the carrier of g, the carrier of g:] -defined the carrier of g -valued Function-like V23([: the carrier of g, the carrier of g:]) quasi_total Element of bool [:[: the carrier of g, the carrier of g:], the carrier of g:]

1. g is left_complementable right_complementable complementable Element of the carrier of g

the OneF of g is left_complementable right_complementable complementable Element of the carrier of g

0. g is V49(g) left_complementable right_complementable complementable Element of the carrier of g

the ZeroF of g is left_complementable right_complementable complementable Element of the carrier of g

h is Element of bool the carrier of g

the addF of g || h is Relation-like Function-like set

[:h,h:] is set

the addF of g | [:h,h:] is Relation-like set

the multF of g || h is Relation-like Function-like set

the multF of g | [:h,h:] is Relation-like set

f1 is non empty doubleLoopStr

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 multF of f1 is non empty Relation-like [: the carrier of f1, the carrier of f1:] -defined the carrier of f1 -valued Function-like V23([: the carrier of f1, the carrier of f1:]) 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 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 g . [h1,g1] is set

the multF of g . (h1,g1) is set

the multF of g . [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 addF of f1 is non empty Relation-like [: the carrier of f1, the carrier of f1:] -defined the carrier of f1 -valued Function-like V23([: the carrier of f1, the carrier of f1:]) quasi_total Element of bool [:[: the carrier of f1, the carrier of f1:], the carrier of f1:]

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 g . [h1,g1] is set

the addF of g . (h1,g1) is set

the addF of g . [h1,g1] is set

F1 is Element of the carrier of f1

hf1 is Element of the carrier of f1

F1 + hf1 is Element of the carrier of f1

the addF of f1 . (F1,hf1) is Element of the carrier of f1

[F1,hf1] is set

{F1,hf1} is non empty set

{F1} is non empty set

{{F1,hf1},{F1}} is non empty set

the addF of f1 . [F1,hf1] is set

gf1 is left_complementable right_complementable complementable Element of the carrier of g

gPh1 is left_complementable right_complementable complementable Element of the carrier of g

gf1 + gPh1 is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (gf1,gPh1) is left_complementable right_complementable complementable Element of the carrier of g

[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 g . [gf1,gPh1] is set

hf1 + F1 is Element of the carrier of f1

the addF of f1 . (hf1,F1) is Element of the carrier of f1

[hf1,F1] is set

{hf1,F1} is non empty set

{hf1} is non empty set

{{hf1,F1},{hf1}} is non empty set

the addF of f1 . [hf1,F1] is set

gPh1 + gf1 is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (gPh1,gf1) is left_complementable right_complementable complementable Element of the carrier of g

[gPh1,gf1] is set

{gPh1,gf1} is non empty set

{gPh1} is non empty set

{{gPh1,gf1},{gPh1}} is non empty set

the addF of g . [gPh1,gf1] is set

F1 is Element of the carrier of f1

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

F1 + (hf1 + gf1) is Element of the carrier of f1

the addF of f1 . (F1,(hf1 + gf1)) is Element of the carrier of f1

[F1,(hf1 + gf1)] is set

{F1,(hf1 + gf1)} is non empty set

{F1} is non empty set

{{F1,(hf1 + gf1)},{F1}} is non empty set

the addF of f1 . [F1,(hf1 + gf1)] is set

gPh1 is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (gPh1,(hf1 + gf1)) is set

[gPh1,(hf1 + gf1)] is set

{gPh1,(hf1 + gf1)} is non empty set

{gPh1} is non empty set

{{gPh1,(hf1 + gf1)},{gPh1}} is non empty set

the addF of g . [gPh1,(hf1 + gf1)] is set

x is left_complementable right_complementable complementable Element of the carrier of g

a is left_complementable right_complementable complementable Element of the carrier of g

x + a is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (x,a) is left_complementable right_complementable complementable Element of the carrier of g

[x,a] is set

{x,a} is non empty set

{x} is non empty set

{{x,a},{x}} is non empty set

the addF of g . [x,a] is set

gPh1 + (x + a) is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (gPh1,(x + a)) is left_complementable right_complementable complementable Element of the carrier of g

[gPh1,(x + a)] is set

{gPh1,(x + a)} is non empty set

{{gPh1,(x + a)},{gPh1}} is non empty set

the addF of g . [gPh1,(x + a)] is set

F1 + hf1 is Element of the carrier of f1

the addF of f1 . (F1,hf1) is Element of the carrier of f1

[F1,hf1] is set

{F1,hf1} is non empty set

{{F1,hf1},{F1}} is non empty set

the addF of f1 . [F1,hf1] is set

(F1 + hf1) + gf1 is Element of the carrier of f1

the addF of f1 . ((F1 + hf1),gf1) is Element of the carrier of f1

[(F1 + hf1),gf1] is set

{(F1 + hf1),gf1} is non empty set

{(F1 + hf1)} is non empty set

{{(F1 + hf1),gf1},{(F1 + hf1)}} is non empty set

the addF of f1 . [(F1 + hf1),gf1] is set

the addF of g . ((F1 + hf1),a) is set

[(F1 + hf1),a] is set

{(F1 + hf1),a} is non empty set

{{(F1 + hf1),a},{(F1 + hf1)}} is non empty set

the addF of g . [(F1 + hf1),a] is set

gPh1 + x is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (gPh1,x) is left_complementable right_complementable complementable Element of the carrier of g

[gPh1,x] is set

{gPh1,x} is non empty set

{{gPh1,x},{gPh1}} is non empty set

the addF of g . [gPh1,x] is set

(gPh1 + x) + a is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . ((gPh1 + x),a) is left_complementable right_complementable complementable Element of the carrier of g

[(gPh1 + x),a] is set

{(gPh1 + x),a} is non empty set

{(gPh1 + x)} is non empty set

{{(gPh1 + x),a},{(gPh1 + x)}} is non empty set

the addF of g . [(gPh1 + x),a] is set

F1 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

F1 + (0. f1) is Element of the carrier of f1

the addF of f1 . (F1,(0. f1)) is Element of the carrier of f1

[F1,(0. f1)] is set

{F1,(0. f1)} is non empty set

{F1} is non empty set

{{F1,(0. f1)},{F1}} is non empty set

the addF of f1 . [F1,(0. f1)] is set

hf1 is left_complementable right_complementable complementable Element of the carrier of g

hf1 + (0. g) is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (hf1,(0. g)) is left_complementable right_complementable complementable Element of the carrier of g

[hf1,(0. g)] is set

{hf1,(0. g)} is non empty set

{hf1} is non empty set

{{hf1,(0. g)},{hf1}} is non empty set

the addF of g . [hf1,(0. g)] is set

F1 is Element of the carrier of f1

hf1 is left_complementable right_complementable complementable Element of the carrier of g

gf1 is left_complementable right_complementable complementable Element of the carrier of g

hf1 + gf1 is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (hf1,gf1) is left_complementable right_complementable complementable Element of the carrier of g

[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 g . [hf1,gf1] is set

- hf1 is left_complementable right_complementable complementable Element of the carrier of g

gPh1 is Element of the carrier of f1

F1 + gPh1 is Element of the carrier of f1

the addF of f1 . (F1,gPh1) is Element of the carrier of f1

[F1,gPh1] is set

{F1,gPh1} is non empty set

{F1} is non empty set

{{F1,gPh1},{F1}} is non empty set

the addF of f1 . [F1,gPh1] is set

gf1 is Element of the carrier of f1

F1 is Element of the carrier of f1

hf1 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

F1 * (hf1 * gf1) is Element of the carrier of f1

the multF of f1 . (F1,(hf1 * gf1)) is Element of the carrier of f1

[F1,(hf1 * gf1)] is set

{F1,(hf1 * gf1)} is non empty set

{F1} is non empty set

{{F1,(hf1 * gf1)},{F1}} is non empty set

the multF of f1 . [F1,(hf1 * gf1)] is set

the multF of g . (F1,(hf1 * gf1)) is set

the multF of g . [F1,(hf1 * gf1)] is set

x is left_complementable right_complementable complementable Element of the carrier of g

a is left_complementable right_complementable complementable Element of the carrier of g

gPh1 is left_complementable right_complementable complementable Element of the carrier of g

a * gPh1 is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . (a,gPh1) is left_complementable right_complementable complementable Element of the carrier of g

[a,gPh1] is set

{a,gPh1} is non empty set

{a} is non empty set

{{a,gPh1},{a}} is non empty set

the multF of g . [a,gPh1] is set

x * (a * gPh1) is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . (x,(a * gPh1)) is left_complementable right_complementable complementable Element of the carrier of g

[x,(a * gPh1)] is set

{x,(a * gPh1)} is non empty set

{x} is non empty set

{{x,(a * gPh1)},{x}} is non empty set

the multF of g . [x,(a * gPh1)] is set

F1 * hf1 is Element of the carrier of f1

the multF of f1 . (F1,hf1) is Element of the carrier of f1

[F1,hf1] is set

{F1,hf1} is non empty set

{{F1,hf1},{F1}} is non empty set

the multF of f1 . [F1,hf1] is set

x * a is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . (x,a) is left_complementable right_complementable complementable Element of the carrier of g

[x,a] is set

{x,a} is non empty set

{{x,a},{x}} is non empty set

the multF of g . [x,a] is set

(F1 * hf1) * gf1 is Element of the carrier of f1

the multF of f1 . ((F1 * hf1),gf1) is Element of the carrier of f1

[(F1 * hf1),gf1] is set

{(F1 * hf1),gf1} is non empty set

{(F1 * hf1)} is non empty set

{{(F1 * hf1),gf1},{(F1 * hf1)}} is non empty set

the multF of f1 . [(F1 * hf1),gf1] is set

(x * a) * gPh1 is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . ((x * a),gPh1) is left_complementable right_complementable complementable Element of the carrier of g

[(x * a),gPh1] is set

{(x * a),gPh1} is non empty set

{(x * a)} is non empty set

{{(x * a),gPh1},{(x * a)}} is non empty set

the multF of g . [(x * a),gPh1] is set

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

F1 * (1. f1) is Element of the carrier of f1

the multF of f1 . (F1,(1. f1)) is Element of the carrier of f1

[F1,(1. f1)] is set

{F1,(1. f1)} is non empty set

{F1} is non empty set

{{F1,(1. f1)},{F1}} is non empty set

the multF of f1 . [F1,(1. f1)] is set

hf1 is left_complementable right_complementable complementable Element of the carrier of g

hf1 * (1. g) is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . (hf1,(1. g)) is left_complementable right_complementable complementable Element of the carrier of g

[hf1,(1. g)] is set

{hf1,(1. g)} is non empty set

{hf1} is non empty set

{{hf1,(1. g)},{hf1}} is non empty set

the multF of g . [hf1,(1. g)] is set

(1. f1) * F1 is Element of the carrier of f1

the multF of f1 . ((1. f1),F1) is Element of the carrier of f1

[(1. f1),F1] is set

{(1. f1),F1} is non empty set

{(1. f1)} is non empty set

{{(1. f1),F1},{(1. f1)}} is non empty set

the multF of f1 . [(1. f1),F1] is set

(1. g) * hf1 is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . ((1. g),hf1) is left_complementable right_complementable complementable Element of the carrier of g

[(1. g),hf1] is set

{(1. g),hf1} is non empty set

{(1. g)} is non empty set

{{(1. g),hf1},{(1. g)}} is non empty set

the multF of g . [(1. g),hf1] is set

hf1 is Element of the carrier of f1

gf1 is Element of the carrier of f1

F1 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

(hf1 + gf1) * F1 is Element of the carrier of f1

the multF of f1 . ((hf1 + gf1),F1) is Element of the carrier of f1

[(hf1 + gf1),F1] is set

{(hf1 + gf1),F1} is non empty set

{(hf1 + gf1)} is non empty set

{{(hf1 + gf1),F1},{(hf1 + gf1)}} is non empty set

the multF of f1 . [(hf1 + gf1),F1] is set

the multF of g . ((hf1 + gf1),F1) is set

the multF of g . [(hf1 + gf1),F1] is set

gPh1 is left_complementable right_complementable complementable Element of the carrier of g

x is left_complementable right_complementable complementable Element of the carrier of g

gPh1 + x is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (gPh1,x) is left_complementable right_complementable complementable Element of the carrier of g

[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 g . [gPh1,x] is set

a is left_complementable right_complementable complementable Element of the carrier of g

(gPh1 + x) * a is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . ((gPh1 + x),a) is left_complementable right_complementable complementable Element of the carrier of g

[(gPh1 + x),a] is set

{(gPh1 + x),a} is non empty set

{(gPh1 + x)} is non empty set

{{(gPh1 + x),a},{(gPh1 + x)}} is non empty set

the multF of g . [(gPh1 + x),a] is set

gPh1 * a is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . (gPh1,a) is left_complementable right_complementable complementable Element of the carrier of g

[gPh1,a] is set

{gPh1,a} is non empty set

{{gPh1,a},{gPh1}} is non empty set

the multF of g . [gPh1,a] is set

x * a is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . (x,a) is left_complementable right_complementable complementable Element of the carrier of g

[x,a] is set

{x,a} is non empty set

{x} is non empty set

{{x,a},{x}} is non empty set

the multF of g . [x,a] is set

(gPh1 * a) + (x * a) is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . ((gPh1 * a),(x * a)) is left_complementable right_complementable complementable Element of the carrier of g

[(gPh1 * a),(x * a)] is set

{(gPh1 * a),(x * a)} is non empty set

{(gPh1 * a)} is non empty set

{{(gPh1 * a),(x * a)},{(gPh1 * a)}} is non empty set

the addF of g . [(gPh1 * a),(x * a)] is set

gf1 * F1 is Element of the carrier of f1

the multF of f1 . (gf1,F1) is Element of the carrier of f1

[gf1,F1] is set

{gf1,F1} is non empty set

{gf1} is non empty set

{{gf1,F1},{gf1}} is non empty set

the multF of f1 . [gf1,F1] is set

the addF of g . (( the multF of g . (gPh1,a)),(gf1 * F1)) is set

[( the multF of g . (gPh1,a)),(gf1 * F1)] is set

{( the multF of g . (gPh1,a)),(gf1 * F1)} is non empty set

{( the multF of g . (gPh1,a))} is non empty set

{{( the multF of g . (gPh1,a)),(gf1 * F1)},{( the multF of g . (gPh1,a))}} is non empty set

the addF of g . [( the multF of g . (gPh1,a)),(gf1 * F1)] is set

hf1 * F1 is Element of the carrier of f1

the multF of f1 . (hf1,F1) is Element of the carrier of f1

[hf1,F1] is set

{hf1,F1} is non empty set

{{hf1,F1},{hf1}} is non empty set

the multF of f1 . [hf1,F1] is set

the addF of g . ((hf1 * F1),(gf1 * F1)) is set

[(hf1 * F1),(gf1 * F1)] is set

{(hf1 * F1),(gf1 * F1)} is non empty set

{(hf1 * F1)} is non empty set

{{(hf1 * F1),(gf1 * F1)},{(hf1 * F1)}} is non empty set

the addF of g . [(hf1 * F1),(gf1 * F1)] is set

F1 * (hf1 + gf1) is Element of the carrier of f1

the multF of f1 . (F1,(hf1 + gf1)) is Element of the carrier of f1

[F1,(hf1 + gf1)] is set

{F1,(hf1 + gf1)} is non empty set

{F1} is non empty set

{{F1,(hf1 + gf1)},{F1}} is non empty set

the multF of f1 . [F1,(hf1 + gf1)] is set

the multF of g . (F1,(hf1 + gf1)) is set

the multF of g . [F1,(hf1 + gf1)] is set

a * (gPh1 + x) is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . (a,(gPh1 + x)) is left_complementable right_complementable complementable Element of the carrier of g

[a,(gPh1 + x)] is set

{a,(gPh1 + x)} is non empty set

{a} is non empty set

{{a,(gPh1 + x)},{a}} is non empty set

the multF of g . [a,(gPh1 + x)] is set

a * gPh1 is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . (a,gPh1) is left_complementable right_complementable complementable Element of the carrier of g

[a,gPh1] is set

{a,gPh1} is non empty set

{{a,gPh1},{a}} is non empty set

the multF of g . [a,gPh1] is set

a * x is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . (a,x) is left_complementable right_complementable complementable Element of the carrier of g

[a,x] is set

{a,x} is non empty set

{{a,x},{a}} is non empty set

the multF of g . [a,x] is set

(a * gPh1) + (a * x) is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . ((a * gPh1),(a * x)) is left_complementable right_complementable complementable Element of the carrier of g

[(a * gPh1),(a * x)] is set

{(a * gPh1),(a * x)} is non empty set

{(a * gPh1)} is non empty set

{{(a * gPh1),(a * x)},{(a * gPh1)}} is non empty set

the addF of g . [(a * gPh1),(a * x)] is set

the multF of g . (F1,gPh1) is set

[F1,gPh1] is set

{F1,gPh1} is non empty set

{{F1,gPh1},{F1}} is non empty set

the multF of g . [F1,gPh1] is set

F1 * gf1 is Element of the carrier of f1

the multF of f1 . (F1,gf1) is Element of the carrier of f1

[F1,gf1] is set

{F1,gf1} is non empty set

{{F1,gf1},{F1}} is non empty set

the multF of f1 . [F1,gf1] is set

the addF of g . (( the multF of g . (F1,gPh1)),(F1 * gf1)) is set

[( the multF of g . (F1,gPh1)),(F1 * gf1)] is set

{( the multF of g . (F1,gPh1)),(F1 * gf1)} is non empty set

{( the multF of g . (F1,gPh1))} is non empty set

{{( the multF of g . (F1,gPh1)),(F1 * gf1)},{( the multF of g . (F1,gPh1))}} is non empty set

the addF of g . [( the multF of g . (F1,gPh1)),(F1 * gf1)] is set

F1 * hf1 is Element of the carrier of f1

the multF of f1 . (F1,hf1) is Element of the carrier of f1

[F1,hf1] is set

{F1,hf1} is non empty set

{{F1,hf1},{F1}} is non empty set

the multF of f1 . [F1,hf1] is set

the addF of g . ((F1 * hf1),(F1 * gf1)) is set

[(F1 * hf1),(F1 * gf1)] is set

{(F1 * hf1),(F1 * gf1)} is non empty set

{(F1 * hf1)} is non empty set

{{(F1 * hf1),(F1 * gf1)},{(F1 * hf1)}} is non empty set

the addF of g . [(F1 * hf1),(F1 * gf1)] is set

(F1 * hf1) + (F1 * gf1) is Element of the carrier of f1

the addF of f1 . ((F1 * hf1),(F1 * gf1)) is Element of the carrier of f1

the addF of f1 . [(F1 * hf1),(F1 * gf1)] is set

(hf1 * F1) + (gf1 * F1) is Element of the carrier of f1

the addF of f1 . ((hf1 * F1),(gf1 * F1)) is Element of the carrier of f1

the addF of f1 . [(hf1 * F1),(gf1 * F1)] 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 left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

[#] X is non empty non proper add-closed (X) (X) Element of bool the carrier of X

the carrier of X is non empty set

bool 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 V23([: the carrier of X, the carrier of X:]) 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 V23([: the carrier of X, the carrier of X:]) 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 left_complementable right_complementable complementable Element of the carrier of X

the OneF of X is left_complementable right_complementable complementable Element of the carrier of X

0. X is V49(X) left_complementable right_complementable complementable Element of the carrier of X

the ZeroF of X is left_complementable right_complementable complementable Element of the carrier of X

doubleLoopStr(# the carrier of X, the addF of X, the multF of X,(1. X),(0. X) #) is non empty strict doubleLoopStr

X is non empty multLoopStr_0

the carrier of X is non empty set

bool the carrier of X is non empty set

X is non empty addLoopStr

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

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 V23([: the carrier of X, the carrier of X:]) 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 || B is Relation-like Function-like set

[:B,B:] is set

the addF of X | [:B,B:] is Relation-like set

[:[:B,B:],B:] is set

bool [:[:B,B:],B:] is non empty set

dom the addF of X is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]

bool [: the carrier of X, the carrier of X:] is non empty set

B is set

( the addF of X || B) . B is set

ONE is set

f is set

[ONE,f] is set

{ONE,f} is non empty set

{ONE} is non empty set

{{ONE,f},{ONE}} is non empty set

dom ( the addF of X || B) is set

h is Element of the carrier of X

g is Element of the carrier of X

h + g is Element of the carrier of X

the addF of X . (h,g) is Element of the carrier of X

[h,g] is set

{h,g} is non empty set

{h} is non empty set

{{h,g},{h}} is non empty set

the addF of X . [h,g] is set

dom ( the addF of X || B) is set

X is non empty multLoopStr_0

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

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 V23([: the carrier of X, the carrier of X:]) 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 || B is Relation-like Function-like set

[:B,B:] is set

the multF of X | [:B,B:] is Relation-like set

[:[:B,B:],B:] is set

bool [:[:B,B:],B:] is non empty set

dom the multF of X is Relation-like the carrier of X -defined the carrier of X -valued Element of bool [: the carrier of X, the carrier of X:]

bool [: the carrier of X, the carrier of X:] is non empty set

B is set

( the multF of X || B) . B is set

ONE is set

f is set

[ONE,f] is set

{ONE,f} is non empty set

{ONE} is non empty set

{{ONE,f},{ONE}} is non empty set

dom ( the multF of X || B) is set

h is Element of the carrier of X

g is Element of the carrier of X

h * g is Element of the carrier of X

the multF of X . (h,g) is Element of the carrier of X

[h,g] is set

{h,g} is non empty set

{h} is non empty set

{{h,g},{h}} is non empty set

the multF of X . [h,g] is set

dom ( the multF of X || B) is set

X is non empty right_complementable add-associative right_zeroed doubleLoopStr

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

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 Element of B is Element of B

ONE is right_complementable Element of the carrier of X

- ONE is right_complementable Element of the carrier of X

ONE + (- ONE) is right_complementable Element of 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 V23([: the carrier of X, the carrier of X:]) 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 . (ONE,(- ONE)) is right_complementable Element of the carrier of X

[ONE,(- ONE)] is set

{ONE,(- ONE)} is non empty set

{ONE} is non empty set

{{ONE,(- ONE)},{ONE}} is non empty set

the addF of X . [ONE,(- ONE)] is set

X is non empty multLoopStr_0

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

1. X is Element of the carrier of X

the OneF of X is Element of the carrier of X

X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed V100() unital associative right-distributive left-distributive right_unital well-unital distributive left_unital doubleLoopStr

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

(X,B) is Relation-like [:B,B:] -defined B -valued Function-like quasi_total Element of bool [:[:B,B:],B:]

[:B,B:] is set

[:[:B,B:],B:] is set

bool [:[:B,B:],B:] is non empty set

(X,B) is Relation-like [:B,B:] -defined B -valued Function-like quasi_total Element of bool [:[:B,B:],B:]

(X,B) is Element of B

(X,B) is Element of B

doubleLoopStr(# B,(X,B),(X,B),(X,B),(X,B) #) is strict doubleLoopStr

1_ X is left_complementable right_complementable complementable Element of the carrier of X

1. X is left_complementable right_complementable complementable Element of the carrier of X

the OneF of X is left_complementable right_complementable complementable Element of the carrier of X

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 V23([: the carrier of X, the carrier of X:]) 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 || B is Relation-like Function-like set

the multF of X | [:B,B:] is Relation-like set

0. X is V49(X) left_complementable right_complementable complementable Element of the carrier of X

the ZeroF of X is left_complementable right_complementable complementable Element of 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 V23([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

the addF of X || B is Relation-like Function-like set

the addF of X | [:B,B:] is Relation-like set

X is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital AlgebraStr

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 V23([: the carrier of X, the carrier of X:]) 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 V23([: the carrier of X, the carrier of X:]) quasi_total Element of bool [:[: the carrier of X, the carrier of X:], the carrier of X:]

[:REAL, the carrier of X:] is non empty set

the Mult of X is non empty Relation-like [:REAL, the carrier of X:] -defined the carrier of X -valued Function-like V23([:REAL, the carrier of X:]) quasi_total Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

[:[:REAL, the carrier of X:], the carrier of X:] is non empty set

bool [:[:REAL, the carrier of X:], the carrier of X:] is non empty set

1. X is left_complementable right_complementable complementable Element of the carrier of X

the OneF of X is left_complementable right_complementable complementable Element of the carrier of X

0. X is V49(X) left_complementable right_complementable complementable Element of the carrier of X

the ZeroF of X is left_complementable right_complementable 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 | [:REAL, the carrier of X:] is Relation-like [:REAL, the carrier of X:] -defined the carrier of X -valued Function-like Element of bool [:[:REAL, the carrier of X:], the carrier of X:]

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

[:REAL,X:] is non empty set

[:[:REAL,X:],X:] is non empty set

bool [:[:REAL,X:],X:] is non empty set

B is Element of X

B is Element of X

ONE is non empty Relation-like [:X,X:] -defined X -valued Function-like V23([:X,X:]) quasi_total Element of bool [:[:X,X:],X:]

f is non empty Relation-like [:X,X:] -defined X -valued Function-like V23([:X,X:]) quasi_total Element of bool [:[:X,X:],X:]

g is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative V100() vector-associative unital associative commutative right-distributive right_unital well-unital left_unital AlgebraStr

the carrier of g is non empty set

bool the carrier of g is non empty set

0. g is V49(g) left_complementable right_complementable complementable Element of the carrier of g

the ZeroF of g is left_complementable right_complementable complementable Element of the carrier of g

1. g is left_complementable right_complementable complementable Element of the carrier of g

the OneF of g is left_complementable right_complementable complementable Element of the carrier of g

the addF of g is non empty Relation-like [: the carrier of g, the carrier of g:] -defined the carrier of g -valued Function-like V23([: the carrier of g, the carrier of g:]) quasi_total Element of bool [:[: the carrier of g, the carrier of g:], the carrier of g:]

[: the carrier of g, the carrier of g:] is non empty set

[:[: the carrier of g, the carrier of g:], the carrier of g:] is non empty set

bool [:[: the carrier of g, the carrier of g:], the carrier of g:] is non empty set

the multF of g is non empty Relation-like [: the carrier of g, the carrier of g:] -defined the carrier of g -valued Function-like V23([: the carrier of g, the carrier of g:]) quasi_total Element of bool [:[: the carrier of g, the carrier of g:], the carrier of g:]

[:REAL, the carrier of g:] is non empty set

the Mult of g is non empty Relation-like [:REAL, the carrier of g:] -defined the carrier of g -valued Function-like V23([:REAL, the carrier of g:]) quasi_total Element of bool [:[:REAL, the carrier of g:], the carrier of g:]

[:[:REAL, the carrier of g:], the carrier of g:] is non empty set

bool [:[:REAL, the carrier of g:], the carrier of g:] is non empty set

h is Element of bool the carrier of g

the addF of g || h is Relation-like Function-like set

[:h,h:] is set

the addF of g | [:h,h:] is Relation-like set

the multF of g || h is Relation-like Function-like set

the multF of g | [:h,h:] is Relation-like set

[:REAL,h:] is set

the Mult of g | [:REAL,h:] is Relation-like [:REAL, the carrier of g:] -defined the carrier of g -valued Function-like Element of bool [:[:REAL, the carrier of g:], the carrier of g:]

f1 is non empty Relation-like [:REAL,X:] -defined X -valued Function-like V23([:REAL,X:]) quasi_total Element of bool [:[:REAL,X:],X:]

AlgebraStr(# X,f,ONE,f1,B,B #) is strict AlgebraStr

h1 is non empty AlgebraStr

the carrier of h1 is non empty set

g1 is Element of the carrier of h1

F1 is Element of the carrier of h1

g1 + F1 is Element of the carrier of h1

the addF of h1 is non empty Relation-like [: the carrier of h1, the carrier of h1:] -defined the carrier of h1 -valued Function-like V23([: the carrier of h1, the carrier of h1:]) quasi_total Element of bool [:[: the carrier of h1, the carrier of h1:], the carrier of h1:]

[: the carrier of h1, the carrier of h1:] is non empty set

[:[: the carrier of h1, the carrier of h1:], the carrier of h1:] is non empty set

bool [:[: the carrier of h1, the carrier of h1:], the carrier of h1:] is non empty set

the addF of h1 . (g1,F1) is Element of the carrier of h1

[g1,F1] is set

{g1,F1} is non empty set

{g1} is non empty set

{{g1,F1},{g1}} is non empty set

the addF of h1 . [g1,F1] is set

[g1,F1] is Element of [: the carrier of h1, the carrier of h1:]

the addF of g . [g1,F1] is set

the addF of g . (g1,F1) is set

the addF of g . [g1,F1] is set

g1 is Element of the carrier of h1

F1 is Element of the carrier of h1

g1 * F1 is Element of the carrier of h1

the multF of h1 is non empty Relation-like [: the carrier of h1, the carrier of h1:] -defined the carrier of h1 -valued Function-like V23([: the carrier of h1, the carrier of h1:]) quasi_total Element of bool [:[: the carrier of h1, the carrier of h1:], the carrier of h1:]

the multF of h1 . (g1,F1) is Element of the carrier of h1

[g1,F1] is set

{g1,F1} is non empty set

{g1} is non empty set

{{g1,F1},{g1}} is non empty set

the multF of h1 . [g1,F1] is set

[g1,F1] is Element of [: the carrier of h1, the carrier of h1:]

the multF of g . [g1,F1] is set

the multF of g . (g1,F1) is set

the multF of g . [g1,F1] is set

F1 is Element of the carrier of h1

g1 is V11() real ext-real Element of REAL

g1 * F1 is Element of the carrier of h1

the Mult of h1 is non empty Relation-like [:REAL, the carrier of h1:] -defined the carrier of h1 -valued Function-like V23([:REAL, the carrier of h1:]) quasi_total Element of bool [:[:REAL, the carrier of h1:], the carrier of h1:]

[:REAL, the carrier of h1:] is non empty set

[:[:REAL, the carrier of h1:], the carrier of h1:] is non empty set

bool [:[:REAL, the carrier of h1:], the carrier of h1:] is non empty set

the Mult of h1 . (g1,F1) is set

[g1,F1] is set

{g1,F1} is non empty set

{g1} is non empty V177() V178() V179() set

{{g1,F1},{g1}} is non empty set

the Mult of h1 . [g1,F1] is set

[g1,F1] is Element of [:REAL, the carrier of h1:]

the Mult of g . [g1,F1] is set

the Mult of g . (g1,F1) is set

the Mult of g . [g1,F1] is set

hf1 is Element of the carrier of h1

gf1 is Element of the carrier of h1

hf1 + gf1 is Element of the carrier of h1

the addF of h1 . (hf1,gf1) is Element of the carrier of h1

[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 h1 . [hf1,gf1] is set

gPh1 is left_complementable right_complementable complementable Element of the carrier of g

x is left_complementable right_complementable complementable Element of the carrier of g

gPh1 + x is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (gPh1,x) is left_complementable right_complementable complementable Element of the carrier of g

[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 g . [gPh1,x] is set

gf1 + hf1 is Element of the carrier of h1

the addF of h1 . (gf1,hf1) is Element of the carrier of h1

[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 h1 . [gf1,hf1] is set

x + gPh1 is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (x,gPh1) is left_complementable right_complementable complementable Element of the carrier of g

[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 g . [x,gPh1] is set

hf1 is Element of the carrier of h1

gf1 is Element of the carrier of h1

gPh1 is Element of the carrier of h1

gf1 + gPh1 is Element of the carrier of h1

the addF of h1 . (gf1,gPh1) is Element of the carrier of h1

[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 h1 . [gf1,gPh1] is set

hf1 + (gf1 + gPh1) is Element of the carrier of h1

the addF of h1 . (hf1,(gf1 + gPh1)) is Element of the carrier of h1

[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 h1 . [hf1,(gf1 + gPh1)] is set

x is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (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 g . [x,(gf1 + gPh1)] is set

a is left_complementable right_complementable complementable Element of the carrier of g

bb is left_complementable right_complementable complementable Element of the carrier of g

a + bb is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (a,bb) is left_complementable right_complementable complementable Element of the carrier of g

[a,bb] is set

{a,bb} is non empty set

{a} is non empty set

{{a,bb},{a}} is non empty set

the addF of g . [a,bb] is set

x + (a + bb) is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (x,(a + bb)) is left_complementable right_complementable complementable Element of the carrier of g

[x,(a + bb)] is set

{x,(a + bb)} is non empty set

{{x,(a + bb)},{x}} is non empty set

the addF of g . [x,(a + bb)] is set

hf1 + gf1 is Element of the carrier of h1

the addF of h1 . (hf1,gf1) is Element of the carrier of h1

[hf1,gf1] is set

{hf1,gf1} is non empty set

{{hf1,gf1},{hf1}} is non empty set

the addF of h1 . [hf1,gf1] is set

(hf1 + gf1) + gPh1 is Element of the carrier of h1

the addF of h1 . ((hf1 + gf1),gPh1) is Element of the carrier of h1

[(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 h1 . [(hf1 + gf1),gPh1] is set

the addF of g . ((hf1 + gf1),bb) is set

[(hf1 + gf1),bb] is set

{(hf1 + gf1),bb} is non empty set

{{(hf1 + gf1),bb},{(hf1 + gf1)}} is non empty set

the addF of g . [(hf1 + gf1),bb] is set

x + a is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (x,a) is left_complementable right_complementable complementable Element of the carrier of g

[x,a] is set

{x,a} is non empty set

{{x,a},{x}} is non empty set

the addF of g . [x,a] is set

(x + a) + bb is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . ((x + a),bb) is left_complementable right_complementable complementable Element of the carrier of g

[(x + a),bb] is set

{(x + a),bb} is non empty set

{(x + a)} is non empty set

{{(x + a),bb},{(x + a)}} is non empty set

the addF of g . [(x + a),bb] is set

hf1 is Element of the carrier of h1

0. h1 is V49(h1) Element of the carrier of h1

the ZeroF of h1 is Element of the carrier of h1

hf1 + (0. h1) is Element of the carrier of h1

the addF of h1 . (hf1,(0. h1)) is Element of the carrier of h1

[hf1,(0. h1)] is set

{hf1,(0. h1)} is non empty set

{hf1} is non empty set

{{hf1,(0. h1)},{hf1}} is non empty set

the addF of h1 . [hf1,(0. h1)] is set

gf1 is left_complementable right_complementable complementable Element of the carrier of g

gf1 + (0. g) is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (gf1,(0. g)) is left_complementable right_complementable complementable Element of the carrier of g

[gf1,(0. g)] is set

{gf1,(0. g)} is non empty set

{gf1} is non empty set

{{gf1,(0. g)},{gf1}} is non empty set

the addF of g . [gf1,(0. g)] is set

hf1 is Element of the carrier of h1

gf1 is left_complementable right_complementable complementable Element of the carrier of g

gPh1 is left_complementable right_complementable complementable Element of the carrier of g

gf1 + gPh1 is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (gf1,gPh1) is left_complementable right_complementable complementable Element of the carrier of g

[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 g . [gf1,gPh1] is set

- gf1 is left_complementable right_complementable complementable Element of the carrier of g

x is Element of the carrier of h1

hf1 + x is Element of the carrier of h1

the addF of h1 . (hf1,x) is Element of the carrier of h1

[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 h1 . [hf1,x] is set

hf1 is Element of the carrier of h1

gf1 is Element of the carrier of h1

hf1 * gf1 is Element of the carrier of h1

the multF of h1 . (hf1,gf1) is Element of the carrier of h1

[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 h1 . [hf1,gf1] is set

gPh1 is left_complementable right_complementable complementable Element of the carrier of g

x is left_complementable right_complementable complementable Element of the carrier of g

gPh1 * x is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . (gPh1,x) is left_complementable right_complementable complementable Element of the carrier of g

[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 g . [gPh1,x] is set

gf1 * hf1 is Element of the carrier of h1

the multF of h1 . (gf1,hf1) is Element of the carrier of h1

[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 h1 . [gf1,hf1] is set

x * gPh1 is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . (x,gPh1) is left_complementable right_complementable complementable Element of the carrier of g

[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 g . [x,gPh1] is set

gPh1 is Element of the carrier of h1

hf1 is Element of the carrier of h1

gf1 is Element of the carrier of h1

gf1 * gPh1 is Element of the carrier of h1

the multF of h1 . (gf1,gPh1) is Element of the carrier of h1

[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 h1 . [gf1,gPh1] is set

hf1 * (gf1 * gPh1) is Element of the carrier of h1

the multF of h1 . (hf1,(gf1 * gPh1)) is Element of the carrier of h1

[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 h1 . [hf1,(gf1 * gPh1)] is set

the multF of g . (hf1,(gf1 * gPh1)) is set

the multF of g . [hf1,(gf1 * gPh1)] is set

a is left_complementable right_complementable complementable Element of the carrier of g

bb is left_complementable right_complementable complementable Element of the carrier of g

x is left_complementable right_complementable complementable Element of the carrier of g

bb * x is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . (bb,x) is left_complementable right_complementable complementable Element of the carrier of g

[bb,x] is set

{bb,x} is non empty set

{bb} is non empty set

{{bb,x},{bb}} is non empty set

the multF of g . [bb,x] is set

a * (bb * x) is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . (a,(bb * x)) is left_complementable right_complementable complementable Element of the carrier of g

[a,(bb * x)] is set

{a,(bb * x)} is non empty set

{a} is non empty set

{{a,(bb * x)},{a}} is non empty set

the multF of g . [a,(bb * x)] is set

hf1 * gf1 is Element of the carrier of h1

the multF of h1 . (hf1,gf1) is Element of the carrier of h1

[hf1,gf1] is set

{hf1,gf1} is non empty set

{{hf1,gf1},{hf1}} is non empty set

the multF of h1 . [hf1,gf1] is set

a * bb is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . (a,bb) is left_complementable right_complementable complementable Element of the carrier of g

[a,bb] is set

{a,bb} is non empty set

{{a,bb},{a}} is non empty set

the multF of g . [a,bb] is set

(hf1 * gf1) * gPh1 is Element of the carrier of h1

the multF of h1 . ((hf1 * gf1),gPh1) is Element of the carrier of h1

[(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 h1 . [(hf1 * gf1),gPh1] is set

(a * bb) * x is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . ((a * bb),x) is left_complementable right_complementable complementable Element of the carrier of g

[(a * bb),x] is set

{(a * bb),x} is non empty set

{(a * bb)} is non empty set

{{(a * bb),x},{(a * bb)}} is non empty set

the multF of g . [(a * bb),x] is set

hf1 is Element of the carrier of h1

1. h1 is Element of the carrier of h1

the OneF of h1 is Element of the carrier of h1

hf1 * (1. h1) is Element of the carrier of h1

the multF of h1 . (hf1,(1. h1)) is Element of the carrier of h1

[hf1,(1. h1)] is set

{hf1,(1. h1)} is non empty set

{hf1} is non empty set

{{hf1,(1. h1)},{hf1}} is non empty set

the multF of h1 . [hf1,(1. h1)] is set

gf1 is left_complementable right_complementable complementable Element of the carrier of g

gf1 * (1. g) is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . (gf1,(1. g)) is left_complementable right_complementable complementable Element of the carrier of g

[gf1,(1. g)] is set

{gf1,(1. g)} is non empty set

{gf1} is non empty set

{{gf1,(1. g)},{gf1}} is non empty set

the multF of g . [gf1,(1. g)] is set

hf1 is Element of the carrier of h1

gf1 is Element of the carrier of h1

gPh1 is Element of the carrier of h1

gf1 + gPh1 is Element of the carrier of h1

the addF of h1 . (gf1,gPh1) is Element of the carrier of h1

[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 h1 . [gf1,gPh1] is set

a is left_complementable right_complementable complementable Element of the carrier of g

bb is left_complementable right_complementable complementable Element of the carrier of g

a + bb is left_complementable right_complementable complementable Element of the carrier of g

the addF of g . (a,bb) is left_complementable right_complementable complementable Element of the carrier of g

[a,bb] is set

{a,bb} is non empty set

{a} is non empty set

{{a,bb},{a}} is non empty set

the addF of g . [a,bb] is set

hf1 * (gf1 + gPh1) is Element of the carrier of h1

the multF of h1 . (hf1,(gf1 + gPh1)) is Element of the carrier of h1

[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 h1 . [hf1,(gf1 + gPh1)] is set

x is left_complementable right_complementable complementable Element of the carrier of g

x * (a + bb) is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . (x,(a + bb)) is left_complementable right_complementable complementable Element of the carrier of g

[x,(a + bb)] is set

{x,(a + bb)} is non empty set

{x} is non empty set

{{x,(a + bb)},{x}} is non empty set

the multF of g . [x,(a + bb)] is set

x * a is left_complementable right_complementable complementable Element of the carrier of g

the multF of g . (x,a) is left_complementable right_complementable complementable Element of the carrier of g

[x,a] is set

{x,<