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