REAL is non empty V40() complex-membered ext-real-membered real-membered V135() set
NAT is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() Element of bool REAL
bool REAL is set
COMPLEX is non empty V40() complex-membered V135() set
RAT is non empty V40() complex-membered ext-real-membered real-membered rational-membered V135() set
INT is non empty V40() complex-membered ext-real-membered real-membered rational-membered integer-membered V135() set
[:COMPLEX,COMPLEX:] is set
bool [:COMPLEX,COMPLEX:] is set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is set
[:REAL,REAL:] is set
bool [:REAL,REAL:] is set
[:[:REAL,REAL:],REAL:] is set
bool [:[:REAL,REAL:],REAL:] is set
[:RAT,RAT:] is set
bool [:RAT,RAT:] is set
[:[:RAT,RAT:],RAT:] is set
bool [:[:RAT,RAT:],RAT:] is set
[:INT,INT:] is set
bool [:INT,INT:] is set
[:[:INT,INT:],INT:] is set
bool [:[:INT,INT:],INT:] is set
[:NAT,NAT:] is set
[:[:NAT,NAT:],NAT:] is set
bool [:[:NAT,NAT:],NAT:] is set
NAT is non empty epsilon-transitive epsilon-connected ordinal complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V135() set
bool NAT is set
bool NAT is set
K258() is set
1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V34() real V36() V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
{} is set
0 is ext-real epsilon-transitive epsilon-connected ordinal natural V34() real V36() V37() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of NAT
addreal is V1() V4([:REAL,REAL:]) V5( REAL ) Function-like V18([:REAL,REAL:], REAL ) Element of bool [:[:REAL,REAL:],REAL:]
multreal is V1() V4([:REAL,REAL:]) V5( REAL ) Function-like V18([:REAL,REAL:], REAL ) Element of bool [:[:REAL,REAL:],REAL:]
addLoopStr(# REAL,addreal,0 #) is non empty strict addLoopStr
() is strict addLoopStr
the carrier of () is non empty set
FR is ext-real V34() real Element of the carrier of ()
H is ext-real V34() real set
G is ext-real V34() real Element of the carrier of ()
f is ext-real V34() real set
FR + G is ext-real V34() real Element of the carrier of ()
the addF of () is V1() V4([: the carrier of (), the carrier of ():]) V5( the carrier of ()) Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set
the addF of () . (FR,G) is ext-real V34() real Element of the carrier of ()
H + f is ext-real V34() real Element of REAL
FR + G is ext-real V34() real Element of REAL
FR is ext-real V34() real Element of the carrier of ()
G is ext-real V34() real Element of the carrier of ()
FR + G is ext-real V34() real Element of the carrier of ()
the addF of () . (FR,G) is ext-real V34() real Element of the carrier of ()
FR + G is ext-real V34() real Element of REAL
G + FR is ext-real V34() real Element of the carrier of ()
the addF of () . (G,FR) is ext-real V34() real Element of the carrier of ()
G + FR is ext-real V34() real Element of REAL
FR is ext-real V34() real Element of the carrier of ()
G is ext-real V34() real Element of the carrier of ()
FR + G is ext-real V34() real Element of the carrier of ()
the addF of () . (FR,G) is ext-real V34() real Element of the carrier of ()
FR + G is ext-real V34() real Element of REAL
H is ext-real V34() real Element of the carrier of ()
(FR + G) + H is ext-real V34() real Element of the carrier of ()
the addF of () . ((FR + G),H) is ext-real V34() real Element of the carrier of ()
(FR + G) + H is ext-real V34() real Element of REAL
G + H is ext-real V34() real Element of the carrier of ()
the addF of () . (G,H) is ext-real V34() real Element of the carrier of ()
G + H is ext-real V34() real Element of REAL
FR + (G + H) is ext-real V34() real Element of the carrier of ()
the addF of () . (FR,(G + H)) is ext-real V34() real Element of the carrier of ()
FR + (G + H) is ext-real V34() real Element of REAL
0. () is ext-real V34() real V70(()) Element of the carrier of ()
the ZeroF of () is ext-real V34() real Element of the carrier of ()
FR is ext-real V34() real Element of the carrier of ()
FR + (0. ()) is ext-real V34() real Element of the carrier of ()
the addF of () . (FR,(0. ())) is ext-real V34() real Element of the carrier of ()
FR + (0. ()) is ext-real V34() real Element of REAL
FR is ext-real V34() real Element of the carrier of ()
G is ext-real V34() real Element of REAL
- G is ext-real V34() real Element of REAL
H is ext-real V34() real Element of the carrier of ()
FR + H is ext-real V34() real Element of the carrier of ()
the addF of () . (FR,H) is ext-real V34() real Element of the carrier of ()
FR + H is ext-real V34() real Element of REAL
FR is ext-real V34() real right_complementable Element of the carrier of ()
G is ext-real V34() real set
- FR is ext-real V34() real right_complementable Element of the carrier of ()
- G is ext-real V34() real Element of REAL
H is ext-real V34() real right_complementable Element of the carrier of ()
H + FR is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (H,FR) is ext-real V34() real right_complementable Element of the carrier of ()
H + FR is ext-real V34() real Element of REAL
0. () is ext-real V34() real V70(()) right_complementable Element of the carrier of ()
the ZeroF of () is ext-real V34() real right_complementable Element of the carrier of ()
- FR is ext-real V34() real Element of REAL
0. () is ext-real V34() real V70(()) right_complementable Element of the carrier of ()
the ZeroF of () is ext-real V34() real right_complementable Element of the carrier of ()
FR is ext-real V34() real right_complementable Element of the carrier of ()
G is ext-real V34() real right_complementable Element of the carrier of ()
FR + G is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (FR,G) is ext-real V34() real right_complementable Element of the carrier of ()
FR + G is ext-real V34() real Element of REAL
G + FR is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (G,FR) is ext-real V34() real right_complementable Element of the carrier of ()
G + FR is ext-real V34() real Element of REAL
H is ext-real V34() real right_complementable Element of the carrier of ()
f is ext-real V34() real right_complementable Element of the carrier of ()
H + f is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (H,f) is ext-real V34() real right_complementable Element of the carrier of ()
H + f is ext-real V34() real Element of REAL
b is ext-real V34() real right_complementable Element of the carrier of ()
(H + f) + b is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . ((H + f),b) is ext-real V34() real right_complementable Element of the carrier of ()
(H + f) + b is ext-real V34() real Element of REAL
f + b is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (f,b) is ext-real V34() real right_complementable Element of the carrier of ()
f + b is ext-real V34() real Element of REAL
H + (f + b) is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (H,(f + b)) is ext-real V34() real right_complementable Element of the carrier of ()
H + (f + b) is ext-real V34() real Element of REAL
x is ext-real V34() real right_complementable Element of the carrier of ()
x + (0. ()) is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (x,(0. ())) is ext-real V34() real right_complementable Element of the carrier of ()
x + (0. ()) is ext-real V34() real Element of REAL
y is ext-real V34() real right_complementable Element of the carrier of ()
- y is ext-real V34() real right_complementable Element of the carrier of ()
- y is ext-real V34() real Element of REAL
y + (- y) is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (y,(- y)) is ext-real V34() real right_complementable Element of the carrier of ()
y + (- y) is ext-real V34() real Element of REAL
doubleLoopStr(# REAL,addreal,multreal,1,0 #) is non empty strict doubleLoopStr
() is strict doubleLoopStr
the carrier of () is non empty set
FR is ext-real V34() real Element of the carrier of ()
H is ext-real V34() real set
G is ext-real V34() real Element of the carrier of ()
f is ext-real V34() real set
FR + G is ext-real V34() real Element of the carrier of ()
the addF of () is V1() V4([: the carrier of (), the carrier of ():]) V5( the carrier of ()) Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set
the addF of () . (FR,G) is ext-real V34() real Element of the carrier of ()
H + f is ext-real V34() real Element of REAL
FR + G is ext-real V34() real Element of REAL
FR is ext-real V34() real Element of the carrier of ()
H is ext-real V34() real set
G is ext-real V34() real Element of the carrier of ()
f is ext-real V34() real set
FR * G is ext-real V34() real Element of the carrier of ()
the multF of () is V1() V4([: the carrier of (), the carrier of ():]) V5( the carrier of ()) Function-like V18([: the carrier of (), the carrier of ():], the carrier of ()) Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
the multF of () . (FR,G) is ext-real V34() real Element of the carrier of ()
H * f is ext-real V34() real Element of REAL
FR * G is ext-real V34() real Element of REAL
FR is non empty multLoopStr
1. FR is Element of the carrier of FR
the carrier of FR is non empty set
the OneF of FR is Element of the carrier of FR
G is Element of the carrier of FR
G * (1. FR) is Element of the carrier of FR
the multF of FR is V1() V4([: the carrier of FR, the carrier of FR:]) V5( the carrier of FR) Function-like V18([: the carrier of FR, the carrier of FR:], the carrier of FR) Element of bool [:[: the carrier of FR, the carrier of FR:], the carrier of FR:]
[: the carrier of FR, the carrier of FR:] is set
[:[: the carrier of FR, the carrier of FR:], the carrier of FR:] is set
bool [:[: the carrier of FR, the carrier of FR:], the carrier of FR:] is set
the multF of FR . (G,(1. FR)) is Element of the carrier of FR
H is Element of the carrier of FR
(1. FR) * H is Element of the carrier of FR
the multF of FR . ((1. FR),H) is Element of the carrier of FR
FR is non empty multLoopStr
1. FR is Element of the carrier of FR
the carrier of FR is non empty set
the OneF of FR is Element of the carrier of FR
1_ FR is Element of the carrier of FR
G is Element of the carrier of FR
G * (1. FR) is Element of the carrier of FR
the multF of FR is V1() V4([: the carrier of FR, the carrier of FR:]) V5( the carrier of FR) Function-like V18([: the carrier of FR, the carrier of FR:], the carrier of FR) Element of bool [:[: the carrier of FR, the carrier of FR:], the carrier of FR:]
[: the carrier of FR, the carrier of FR:] is set
[:[: the carrier of FR, the carrier of FR:], the carrier of FR:] is set
bool [:[: the carrier of FR, the carrier of FR:], the carrier of FR:] is set
the multF of FR . (G,(1. FR)) is Element of the carrier of FR
H is Element of the carrier of FR
(1. FR) * H is Element of the carrier of FR
the multF of FR . ((1. FR),H) is Element of the carrier of FR
FR is ext-real V34() real Element of the carrier of ()
1. () is ext-real V34() real Element of the carrier of ()
the OneF of () is ext-real V34() real Element of the carrier of ()
FR * (1. ()) is ext-real V34() real Element of the carrier of ()
the multF of () . (FR,(1. ())) is ext-real V34() real Element of the carrier of ()
FR * (1. ()) is ext-real V34() real Element of REAL
(1. ()) * FR is ext-real V34() real Element of the carrier of ()
the multF of () . ((1. ()),FR) is ext-real V34() real Element of the carrier of ()
(1. ()) * FR is ext-real V34() real Element of REAL
FR is non empty multLoopStr_0
the carrier of FR is non empty set
0. FR is V70(FR) Element of the carrier of FR
the ZeroF of FR is Element of the carrier of FR
1. FR is Element of the carrier of FR
the OneF of FR is Element of the carrier of FR
G is Element of the carrier of FR
G is Element of the carrier of FR
G is ext-real V34() real Element of the carrier of ()
H is ext-real V34() real Element of the carrier of ()
H * G is ext-real V34() real Element of the carrier of ()
the multF of () . (H,G) is ext-real V34() real Element of the carrier of ()
H * G is ext-real V34() real Element of REAL
f is ext-real V34() real Element of the carrier of ()
G * f is ext-real V34() real Element of the carrier of ()
the multF of () . (G,f) is ext-real V34() real Element of the carrier of ()
G * f is ext-real V34() real Element of REAL
G is ext-real V34() real Element of the carrier of ()
H is ext-real V34() real Element of the carrier of ()
G + H is ext-real V34() real Element of the carrier of ()
the addF of () . (G,H) is ext-real V34() real Element of the carrier of ()
G + H is ext-real V34() real Element of REAL
f is ext-real V34() real Element of the carrier of ()
(G + H) + f is ext-real V34() real Element of the carrier of ()
the addF of () . ((G + H),f) is ext-real V34() real Element of the carrier of ()
(G + H) + f is ext-real V34() real Element of REAL
H + f is ext-real V34() real Element of the carrier of ()
the addF of () . (H,f) is ext-real V34() real Element of the carrier of ()
H + f is ext-real V34() real Element of REAL
G + (H + f) is ext-real V34() real Element of the carrier of ()
the addF of () . (G,(H + f)) is ext-real V34() real Element of the carrier of ()
G + (H + f) is ext-real V34() real Element of REAL
0. () is ext-real V34() real V70(()) Element of the carrier of ()
the ZeroF of () is ext-real V34() real Element of the carrier of ()
G is ext-real V34() real Element of the carrier of ()
G + (0. ()) is ext-real V34() real Element of the carrier of ()
the addF of () . (G,(0. ())) is ext-real V34() real Element of the carrier of ()
G + (0. ()) is ext-real V34() real Element of REAL
G is ext-real V34() real Element of the carrier of ()
H is ext-real V34() real Element of REAL
- H is ext-real V34() real Element of REAL
f is ext-real V34() real Element of the carrier of ()
G + f is ext-real V34() real Element of the carrier of ()
the addF of () . (G,f) is ext-real V34() real Element of the carrier of ()
G + f is ext-real V34() real Element of REAL
G is ext-real V34() real Element of the carrier of ()
H is ext-real V34() real Element of the carrier of ()
G + H is ext-real V34() real Element of the carrier of ()
the addF of () . (G,H) is ext-real V34() real Element of the carrier of ()
G + H is ext-real V34() real Element of REAL
H + G is ext-real V34() real Element of the carrier of ()
the addF of () . (H,G) is ext-real V34() real Element of the carrier of ()
H + G is ext-real V34() real Element of REAL
G is ext-real V34() real Element of the carrier of ()
H is ext-real V34() real Element of the carrier of ()
G * H is ext-real V34() real Element of the carrier of ()
the multF of () . (G,H) is ext-real V34() real Element of the carrier of ()
G * H is ext-real V34() real Element of REAL
H * G is ext-real V34() real Element of the carrier of ()
the multF of () . (H,G) is ext-real V34() real Element of the carrier of ()
H * G is ext-real V34() real Element of REAL
G is ext-real V34() real Element of the carrier of ()
H is ext-real V34() real Element of the carrier of ()
G * H is ext-real V34() real Element of the carrier of ()
the multF of () . (G,H) is ext-real V34() real Element of the carrier of ()
G * H is ext-real V34() real Element of REAL
f is ext-real V34() real Element of the carrier of ()
(G * H) * f is ext-real V34() real Element of the carrier of ()
the multF of () . ((G * H),f) is ext-real V34() real Element of the carrier of ()
(G * H) * f is ext-real V34() real Element of REAL
H * f is ext-real V34() real Element of the carrier of ()
the multF of () . (H,f) is ext-real V34() real Element of the carrier of ()
H * f is ext-real V34() real Element of REAL
G * (H * f) is ext-real V34() real Element of the carrier of ()
the multF of () . (G,(H * f)) is ext-real V34() real Element of the carrier of ()
G * (H * f) is ext-real V34() real Element of REAL
1. () is ext-real V34() real Element of the carrier of ()
the OneF of () is ext-real V34() real Element of the carrier of ()
G is ext-real V34() real Element of the carrier of ()
(1. ()) * G is ext-real V34() real Element of the carrier of ()
the multF of () . ((1. ()),G) is ext-real V34() real Element of the carrier of ()
(1. ()) * G is ext-real V34() real Element of REAL
G is ext-real V34() real Element of the carrier of ()
G * (1. ()) is ext-real V34() real Element of the carrier of ()
the multF of () . (G,(1. ())) is ext-real V34() real Element of the carrier of ()
G * (1. ()) is ext-real V34() real Element of REAL
G is ext-real V34() real Element of the carrier of ()
H is ext-real V34() real Element of the carrier of ()
f is ext-real V34() real Element of the carrier of ()
H + f is ext-real V34() real Element of the carrier of ()
the addF of () . (H,f) is ext-real V34() real Element of the carrier of ()
H + f is ext-real V34() real Element of REAL
G * (H + f) is ext-real V34() real Element of the carrier of ()
the multF of () . (G,(H + f)) is ext-real V34() real Element of the carrier of ()
G * (H + f) is ext-real V34() real Element of REAL
G * H is ext-real V34() real Element of the carrier of ()
the multF of () . (G,H) is ext-real V34() real Element of the carrier of ()
G * H is ext-real V34() real Element of REAL
G * f is ext-real V34() real Element of the carrier of ()
the multF of () . (G,f) is ext-real V34() real Element of the carrier of ()
G * f is ext-real V34() real Element of REAL
(G * H) + (G * f) is ext-real V34() real Element of the carrier of ()
the addF of () . ((G * H),(G * f)) is ext-real V34() real Element of the carrier of ()
(G * H) + (G * f) is ext-real V34() real Element of REAL
x is ext-real V34() real Element of the carrier of ()
y is ext-real V34() real Element of the carrier of ()
x + y is ext-real V34() real Element of the carrier of ()
the addF of () . (x,y) is ext-real V34() real Element of the carrier of ()
x + y is ext-real V34() real Element of REAL
b is ext-real V34() real Element of the carrier of ()
(x + y) * b is ext-real V34() real Element of the carrier of ()
the multF of () . ((x + y),b) is ext-real V34() real Element of the carrier of ()
(x + y) * b is ext-real V34() real Element of REAL
x * b is ext-real V34() real Element of the carrier of ()
the multF of () . (x,b) is ext-real V34() real Element of the carrier of ()
x * b is ext-real V34() real Element of REAL
y * b is ext-real V34() real Element of the carrier of ()
the multF of () . (y,b) is ext-real V34() real Element of the carrier of ()
y * b is ext-real V34() real Element of REAL
(x * b) + (y * b) is ext-real V34() real Element of the carrier of ()
the addF of () . ((x * b),(y * b)) is ext-real V34() real Element of the carrier of ()
(x * b) + (y * b) is ext-real V34() real Element of REAL
G is ext-real V34() real Element of the carrier of ()
H is ext-real V34() real Element of REAL
H " is ext-real V34() real Element of REAL
f is ext-real V34() real Element of the carrier of ()
b is ext-real V34() real Element of the carrier of ()
b * G is ext-real V34() real Element of the carrier of ()
the multF of () . (b,G) is ext-real V34() real Element of the carrier of ()
b * G is ext-real V34() real Element of REAL
G is ext-real V34() real right_complementable Element of the carrier of ()
H is ext-real V34() real set
- G is ext-real V34() real right_complementable Element of the carrier of ()
- H is ext-real V34() real Element of REAL
f is ext-real V34() real right_complementable Element of the carrier of ()
f + G is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (f,G) is ext-real V34() real right_complementable Element of the carrier of ()
f + G is ext-real V34() real Element of REAL
0. () is ext-real V34() real V70(()) right_complementable Element of the carrier of ()
the ZeroF of () is ext-real V34() real right_complementable Element of the carrier of ()
- G is ext-real V34() real Element of REAL
G is non empty doubleLoopStr
the carrier of G is non empty set
H is Element of the carrier of G
f is Element of the carrier of G
b is Element of the carrier of G
f + b is Element of the carrier of G
the addF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the addF of G . (f,b) is Element of the carrier of G
H * (f + b) is Element of the carrier of G
the multF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
the multF of G . (H,(f + b)) is Element of the carrier of G
H * f is Element of the carrier of G
the multF of G . (H,f) is Element of the carrier of G
H * b is Element of the carrier of G
the multF of G . (H,b) is Element of the carrier of G
(H * f) + (H * b) is Element of the carrier of G
the addF of G . ((H * f),(H * b)) is Element of the carrier of G
f is Element of the carrier of G
b is Element of the carrier of G
f + b is Element of the carrier of G
the addF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the addF of G . (f,b) is Element of the carrier of G
H is Element of the carrier of G
(f + b) * H is Element of the carrier of G
the multF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
the multF of G . ((f + b),H) is Element of the carrier of G
f * H is Element of the carrier of G
the multF of G . (f,H) is Element of the carrier of G
b * H is Element of the carrier of G
the multF of G . (b,H) is Element of the carrier of G
(f * H) + (b * H) is Element of the carrier of G
the addF of G . ((f * H),(b * H)) is Element of the carrier of G
G is non empty doubleLoopStr
G is non empty doubleLoopStr
the carrier of G is non empty set
H is Element of the carrier of G
f is Element of the carrier of G
b is Element of the carrier of G
f + b is Element of the carrier of G
the addF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the addF of G . (f,b) is Element of the carrier of G
H * (f + b) is Element of the carrier of G
the multF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
the multF of G . (H,(f + b)) is Element of the carrier of G
H * f is Element of the carrier of G
the multF of G . (H,f) is Element of the carrier of G
H * b is Element of the carrier of G
the multF of G . (H,b) is Element of the carrier of G
(H * f) + (H * b) is Element of the carrier of G
the addF of G . ((H * f),(H * b)) is Element of the carrier of G
y is Element of the carrier of G
c8 is Element of the carrier of G
y + c8 is Element of the carrier of G
the addF of G . (y,c8) is Element of the carrier of G
x is Element of the carrier of G
(y + c8) * x is Element of the carrier of G
the multF of G . ((y + c8),x) is Element of the carrier of G
y * x is Element of the carrier of G
the multF of G . (y,x) is Element of the carrier of G
c8 * x is Element of the carrier of G
the multF of G . (c8,x) is Element of the carrier of G
(y * x) + (c8 * x) is Element of the carrier of G
the addF of G . ((y * x),(c8 * x)) is Element of the carrier of G
G is non empty multLoopStr
the carrier of G is non empty set
1. G is Element of the carrier of G
the OneF of G is Element of the carrier of G
H is Element of the carrier of G
(1. G) * H is Element of the carrier of G
the multF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((1. G),H) is Element of the carrier of G
H is Element of the carrier of G
H * (1. G) is Element of the carrier of G
the multF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,(1. G)) is Element of the carrier of G
G is non empty multLoopStr
the carrier of G is non empty set
1. G is Element of the carrier of G
the OneF of G is Element of the carrier of G
H is Element of the carrier of G
H * (1. G) is Element of the carrier of G
the multF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,(1. G)) is Element of the carrier of G
f is Element of the carrier of G
(1. G) * f is Element of the carrier of G
the multF of G . ((1. G),f) is Element of the carrier of G
1. () is ext-real V34() real V70(()) right_complementable Element of the carrier of ()
the OneF of () is ext-real V34() real right_complementable Element of the carrier of ()
0. () is ext-real V34() real V70(()) right_complementable Element of the carrier of ()
the ZeroF of () is ext-real V34() real right_complementable Element of the carrier of ()
G is ext-real V34() real right_complementable Element of the carrier of ()
H is ext-real V34() real right_complementable Element of the carrier of ()
G + H is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (G,H) is ext-real V34() real right_complementable Element of the carrier of ()
G + H is ext-real V34() real Element of REAL
H + G is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (H,G) is ext-real V34() real right_complementable Element of the carrier of ()
H + G is ext-real V34() real Element of REAL
f is ext-real V34() real right_complementable Element of the carrier of ()
b is ext-real V34() real right_complementable Element of the carrier of ()
f + b is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (f,b) is ext-real V34() real right_complementable Element of the carrier of ()
f + b is ext-real V34() real Element of REAL
x is ext-real V34() real right_complementable Element of the carrier of ()
(f + b) + x is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . ((f + b),x) is ext-real V34() real right_complementable Element of the carrier of ()
(f + b) + x is ext-real V34() real Element of REAL
b + x is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (b,x) is ext-real V34() real right_complementable Element of the carrier of ()
b + x is ext-real V34() real Element of REAL
f + (b + x) is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (f,(b + x)) is ext-real V34() real right_complementable Element of the carrier of ()
f + (b + x) is ext-real V34() real Element of REAL
y is ext-real V34() real right_complementable Element of the carrier of ()
y + (0. ()) is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (y,(0. ())) is ext-real V34() real right_complementable Element of the carrier of ()
y + (0. ()) is ext-real V34() real Element of REAL
c8 is ext-real V34() real right_complementable Element of the carrier of ()
- c8 is ext-real V34() real right_complementable Element of the carrier of ()
- c8 is ext-real V34() real Element of REAL
c8 + (- c8) is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (c8,(- c8)) is ext-real V34() real right_complementable Element of the carrier of ()
c8 + (- c8) is ext-real V34() real Element of REAL
y is ext-real V34() real right_complementable Element of the carrier of ()
z is ext-real V34() real right_complementable Element of the carrier of ()
y * z is ext-real V34() real right_complementable Element of the carrier of ()
the multF of () . (y,z) is ext-real V34() real right_complementable Element of the carrier of ()
y * z is ext-real V34() real Element of REAL
z * y is ext-real V34() real right_complementable Element of the carrier of ()
the multF of () . (z,y) is ext-real V34() real right_complementable Element of the carrier of ()
z * y is ext-real V34() real Element of REAL
c11 is ext-real V34() real right_complementable Element of the carrier of ()
c12 is ext-real V34() real right_complementable Element of the carrier of ()
c11 * c12 is ext-real V34() real right_complementable Element of the carrier of ()
the multF of () . (c11,c12) is ext-real V34() real right_complementable Element of the carrier of ()
c11 * c12 is ext-real V34() real Element of REAL
c13 is ext-real V34() real right_complementable Element of the carrier of ()
(c11 * c12) * c13 is ext-real V34() real right_complementable Element of the carrier of ()
the multF of () . ((c11 * c12),c13) is ext-real V34() real right_complementable Element of the carrier of ()
(c11 * c12) * c13 is ext-real V34() real Element of REAL
c12 * c13 is ext-real V34() real right_complementable Element of the carrier of ()
the multF of () . (c12,c13) is ext-real V34() real right_complementable Element of the carrier of ()
c12 * c13 is ext-real V34() real Element of REAL
c11 * (c12 * c13) is ext-real V34() real right_complementable Element of the carrier of ()
the multF of () . (c11,(c12 * c13)) is ext-real V34() real right_complementable Element of the carrier of ()
c11 * (c12 * c13) is ext-real V34() real Element of REAL
c14 is ext-real V34() real right_complementable Element of the carrier of ()
(1. ()) * c14 is ext-real V34() real right_complementable Element of the carrier of ()
the multF of () . ((1. ()),c14) is ext-real V34() real right_complementable Element of the carrier of ()
(1. ()) * c14 is ext-real V34() real Element of REAL
c15 is ext-real V34() real right_complementable Element of the carrier of ()
c16 is ext-real V34() real right_complementable Element of the carrier of ()
c17 is ext-real V34() real right_complementable Element of the carrier of ()
c18 is ext-real V34() real right_complementable Element of the carrier of ()
c17 + c18 is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (c17,c18) is ext-real V34() real right_complementable Element of the carrier of ()
c17 + c18 is ext-real V34() real Element of REAL
c16 * (c17 + c18) is ext-real V34() real right_complementable Element of the carrier of ()
the multF of () . (c16,(c17 + c18)) is ext-real V34() real right_complementable Element of the carrier of ()
c16 * (c17 + c18) is ext-real V34() real Element of REAL
c16 * c17 is ext-real V34() real right_complementable Element of the carrier of ()
the multF of () . (c16,c17) is ext-real V34() real right_complementable Element of the carrier of ()
c16 * c17 is ext-real V34() real Element of REAL
c16 * c18 is ext-real V34() real right_complementable Element of the carrier of ()
the multF of () . (c16,c18) is ext-real V34() real right_complementable Element of the carrier of ()
c16 * c18 is ext-real V34() real Element of REAL
(c16 * c17) + (c16 * c18) is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . ((c16 * c17),(c16 * c18)) is ext-real V34() real right_complementable Element of the carrier of ()
(c16 * c17) + (c16 * c18) is ext-real V34() real Element of REAL
c20 is ext-real V34() real right_complementable Element of the carrier of ()
c21 is ext-real V34() real right_complementable Element of the carrier of ()
c20 + c21 is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . (c20,c21) is ext-real V34() real right_complementable Element of the carrier of ()
c20 + c21 is ext-real V34() real Element of REAL
c19 is ext-real V34() real right_complementable Element of the carrier of ()
(c20 + c21) * c19 is ext-real V34() real right_complementable Element of the carrier of ()
the multF of () . ((c20 + c21),c19) is ext-real V34() real right_complementable Element of the carrier of ()
(c20 + c21) * c19 is ext-real V34() real Element of REAL
c20 * c19 is ext-real V34() real right_complementable Element of the carrier of ()
the multF of () . (c20,c19) is ext-real V34() real right_complementable Element of the carrier of ()
c20 * c19 is ext-real V34() real Element of REAL
c21 * c19 is ext-real V34() real right_complementable Element of the carrier of ()
the multF of () . (c21,c19) is ext-real V34() real right_complementable Element of the carrier of ()
c21 * c19 is ext-real V34() real Element of REAL
(c20 * c19) + (c21 * c19) is ext-real V34() real right_complementable Element of the carrier of ()
the addF of () . ((c20 * c19),(c21 * c19)) is ext-real V34() real right_complementable Element of the carrier of ()
(c20 * c19) + (c21 * c19) is ext-real V34() real Element of REAL
H is non empty doubleLoopStr
the carrier of H is non empty set
G is non empty doubleLoopStr
the carrier of G is non empty set
0. G is V70(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
1. G is Element of the carrier of G
the OneF of G is Element of the carrier of G
f is Element of the carrier of H
0. H is V70(H) Element of the carrier of H
the ZeroF of H is Element of the carrier of H
1. H is Element of the carrier of H
the OneF of H is Element of the carrier of H
b is Element of the carrier of H
x is Element of the carrier of H
y is Element of the carrier of H
x + y is Element of the carrier of H
the addF of H is V1() V4([: the carrier of H, the carrier of H:]) V5( the carrier of H) Function-like V18([: the carrier of H, the carrier of H:], the carrier of H) Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
[: the carrier of H, the carrier of H:] is set
[:[: the carrier of H, the carrier of H:], the carrier of H:] is set
bool [:[: the carrier of H, the carrier of H:], the carrier of H:] is set
the addF of H . (x,y) is Element of the carrier of H
b * (x + y) is Element of the carrier of H
the multF of H is V1() V4([: the carrier of H, the carrier of H:]) V5( the carrier of H) Function-like V18([: the carrier of H, the carrier of H:], the carrier of H) Element of bool [:[: the carrier of H, the carrier of H:], the carrier of H:]
the multF of H . (b,(x + y)) is Element of the carrier of H
b * x is Element of the carrier of H
the multF of H . (b,x) is Element of the carrier of H
b * y is Element of the carrier of H
the multF of H . (b,y) is Element of the carrier of H
(b * x) + (b * y) is Element of the carrier of H
the addF of H . ((b * x),(b * y)) is Element of the carrier of H
y is Element of the carrier of H
z is Element of the carrier of H
y + z is Element of the carrier of H
the addF of H . (y,z) is Element of the carrier of H
c8 is Element of the carrier of H
(y + z) * c8 is Element of the carrier of H
the multF of H . ((y + z),c8) is Element of the carrier of H
y * c8 is Element of the carrier of H
the multF of H . (y,c8) is Element of the carrier of H
z * c8 is Element of the carrier of H
the multF of H . (z,c8) is Element of the carrier of H
(y * c8) + (z * c8) is Element of the carrier of H
the addF of H . ((y * c8),(z * c8)) is Element of the carrier of H
G is non empty multLoopStr
G is non empty almost_left_invertible unital associative commutative () () () () () () doubleLoopStr
the carrier of G is non empty set
0. G is V70(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
H is Element of the carrier of G
f is Element of the carrier of G
H * f is Element of the carrier of G
the multF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,f) is Element of the carrier of G
b is Element of the carrier of G
H * b is Element of the carrier of G
the multF of G . (H,b) is Element of the carrier of G
1. G is Element of the carrier of G
the OneF of G is Element of the carrier of G
x is Element of the carrier of G
x * H is Element of the carrier of G
the multF of G . (x,H) is Element of the carrier of G
(x * H) * f is Element of the carrier of G
the multF of G . ((x * H),f) is Element of the carrier of G
x * (H * f) is Element of the carrier of G
the multF of G . (x,(H * f)) is Element of the carrier of G
x * (H * b) is Element of the carrier of G
the multF of G . (x,(H * b)) is Element of the carrier of G
(x * H) * b is Element of the carrier of G
the multF of G . ((x * H),b) is Element of the carrier of G
H * x is Element of the carrier of G
the multF of G . (H,x) is Element of the carrier of G
(H * x) * f is Element of the carrier of G
the multF of G . ((H * x),f) is Element of the carrier of G
G is non empty almost_left_invertible unital associative commutative () () () doubleLoopStr
the carrier of G is non empty set
H is Element of the carrier of G
0. G is V70(G) Element of the carrier of G
the ZeroF of G is Element of the carrier of G
H " is Element of the carrier of G
1. G is Element of the carrier of G
the OneF of G is Element of the carrier of G
f is Element of the carrier of G
f * H is Element of the carrier of G
the multF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (f,H) is Element of the carrier of G
b is Element of the carrier of G
b * H is Element of the carrier of G
the multF of G . (b,H) is Element of the carrier of G
x is Element of the carrier of G
x * H is Element of the carrier of G
the multF of G . (x,H) is Element of the carrier of G
y is Element of the carrier of G
y * H is Element of the carrier of G
the multF of G . (y,H) is Element of the carrier of G
x * H is Element of the carrier of G
y * H is Element of the carrier of G
x * (1. G) is Element of the carrier of G
the multF of G . (x,(1. G)) is Element of the carrier of G
(y * H) * b is Element of the carrier of G
the multF of G . ((y * H),b) is Element of the carrier of G
y * (1. G) is Element of the carrier of G
the multF of G . (y,(1. G)) is Element of the carrier of G
G is non empty almost_left_invertible unital associative commutative () () () () () () doubleLoopStr
the carrier of G is non empty set
H is Element of the carrier of G
f is Element of the carrier of G
f " is Element of the carrier of G
H * (f ") is Element of the carrier of G
the multF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,(f ")) is Element of the carrier of G
G is non empty right_complementable add-associative right_zeroed () doubleLoopStr
the carrier of G is non empty set
0. G is V70(G) right_complementable Element of the carrier of G
the ZeroF of G is right_complementable Element of the carrier of G
H is right_complementable Element of the carrier of G
H * (0. G) is right_complementable Element of the carrier of G
the multF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,(0. G)) is right_complementable Element of the carrier of G
(H * (0. G)) + (0. G) is right_complementable Element of the carrier of G
the addF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
the addF of G . ((H * (0. G)),(0. G)) is right_complementable Element of the carrier of G
(0. G) + (0. G) is right_complementable Element of the carrier of G
the addF of G . ((0. G),(0. G)) is right_complementable Element of the carrier of G
H * ((0. G) + (0. G)) is right_complementable Element of the carrier of G
the multF of G . (H,((0. G) + (0. G))) is right_complementable Element of the carrier of G
(H * ((0. G) + (0. G))) + (0. G) is right_complementable Element of the carrier of G
the addF of G . ((H * ((0. G) + (0. G))),(0. G)) is right_complementable Element of the carrier of G
(H * (0. G)) + (H * (0. G)) is right_complementable Element of the carrier of G
the addF of G . ((H * (0. G)),(H * (0. G))) is right_complementable Element of the carrier of G
G is non empty right_complementable add-associative right_zeroed () doubleLoopStr
the carrier of G is non empty set
0. G is V70(G) right_complementable Element of the carrier of G
the ZeroF of G is right_complementable Element of the carrier of G
H is right_complementable Element of the carrier of G
(0. G) * H is right_complementable Element of the carrier of G
the multF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((0. G),H) is right_complementable Element of the carrier of G
((0. G) * H) + (0. G) is right_complementable Element of the carrier of G
the addF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
the addF of G . (((0. G) * H),(0. G)) is right_complementable Element of the carrier of G
(0. G) + (0. G) is right_complementable Element of the carrier of G
the addF of G . ((0. G),(0. G)) is right_complementable Element of the carrier of G
((0. G) + (0. G)) * H is right_complementable Element of the carrier of G
the multF of G . (((0. G) + (0. G)),H) is right_complementable Element of the carrier of G
(((0. G) + (0. G)) * H) + (0. G) is right_complementable Element of the carrier of G
the addF of G . ((((0. G) + (0. G)) * H),(0. G)) is right_complementable Element of the carrier of G
((0. G) * H) + ((0. G) * H) is right_complementable Element of the carrier of G
the addF of G . (((0. G) * H),((0. G) * H)) is right_complementable Element of the carrier of G
G is non empty right_complementable add-associative right_zeroed () doubleLoopStr
the carrier of G is non empty set
H is right_complementable Element of the carrier of G
f is right_complementable Element of the carrier of G
- f is right_complementable Element of the carrier of G
H * (- f) is right_complementable Element of the carrier of G
the multF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,(- f)) is right_complementable Element of the carrier of G
H * f is right_complementable Element of the carrier of G
the multF of G . (H,f) is right_complementable Element of the carrier of G
- (H * f) is right_complementable Element of the carrier of G
(H * f) + (H * (- f)) is right_complementable Element of the carrier of G
the addF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
the addF of G . ((H * f),(H * (- f))) is right_complementable Element of the carrier of G
f + (- f) is right_complementable Element of the carrier of G
the addF of G . (f,(- f)) is right_complementable Element of the carrier of G
H * (f + (- f)) is right_complementable Element of the carrier of G
the multF of G . (H,(f + (- f))) is right_complementable Element of the carrier of G
0. G is V70(G) right_complementable Element of the carrier of G
the ZeroF of G is right_complementable Element of the carrier of G
H * (0. G) is right_complementable Element of the carrier of G
the multF of G . (H,(0. G)) is right_complementable Element of the carrier of G
G is non empty right_complementable add-associative right_zeroed () doubleLoopStr
the carrier of G is non empty set
H is right_complementable Element of the carrier of G
- H is right_complementable Element of the carrier of G
f is right_complementable Element of the carrier of G
(- H) * f is right_complementable Element of the carrier of G
the multF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((- H),f) is right_complementable Element of the carrier of G
H * f is right_complementable Element of the carrier of G
the multF of G . (H,f) is right_complementable Element of the carrier of G
- (H * f) is right_complementable Element of the carrier of G
(H * f) + ((- H) * f) is right_complementable Element of the carrier of G
the addF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
the addF of G . ((H * f),((- H) * f)) is right_complementable Element of the carrier of G
H + (- H) is right_complementable Element of the carrier of G
the addF of G . (H,(- H)) is right_complementable Element of the carrier of G
(H + (- H)) * f is right_complementable Element of the carrier of G
the multF of G . ((H + (- H)),f) is right_complementable Element of the carrier of G
0. G is V70(G) right_complementable Element of the carrier of G
the ZeroF of G is right_complementable Element of the carrier of G
(0. G) * f is right_complementable Element of the carrier of G
the multF of G . ((0. G),f) is right_complementable Element of the carrier of G
G is non empty right_complementable add-associative right_zeroed () () () doubleLoopStr
the carrier of G is non empty set
H is right_complementable Element of the carrier of G
- H is right_complementable Element of the carrier of G
f is right_complementable Element of the carrier of G
- f is right_complementable Element of the carrier of G
(- H) * (- f) is right_complementable Element of the carrier of G
the multF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . ((- H),(- f)) is right_complementable Element of the carrier of G
H * f is right_complementable Element of the carrier of G
the multF of G . (H,f) is right_complementable Element of the carrier of G
H * (- f) is right_complementable Element of the carrier of G
the multF of G . (H,(- f)) is right_complementable Element of the carrier of G
- (H * (- f)) is right_complementable Element of the carrier of G
- (H * f) is right_complementable Element of the carrier of G
- (- (H * f)) is right_complementable Element of the carrier of G
G is non empty right_complementable add-associative right_zeroed () doubleLoopStr
the carrier of G is non empty set
H is right_complementable Element of the carrier of G
f is right_complementable Element of the carrier of G
b is right_complementable Element of the carrier of G
f - b is right_complementable Element of the carrier of G
- b is right_complementable Element of the carrier of G
f + (- b) is right_complementable Element of the carrier of G
the addF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the addF of G . (f,(- b)) is right_complementable Element of the carrier of G
H * (f - b) is right_complementable Element of the carrier of G
the multF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
the multF of G . (H,(f - b)) is right_complementable Element of the carrier of G
H * f is right_complementable Element of the carrier of G
the multF of G . (H,f) is right_complementable Element of the carrier of G
H * b is right_complementable Element of the carrier of G
the multF of G . (H,b) is right_complementable Element of the carrier of G
(H * f) - (H * b) is right_complementable Element of the carrier of G
- (H * b) is right_complementable Element of the carrier of G
(H * f) + (- (H * b)) is right_complementable Element of the carrier of G
the addF of G . ((H * f),(- (H * b))) is right_complementable Element of the carrier of G
H * (- b) is right_complementable Element of the carrier of G
the multF of G . (H,(- b)) is right_complementable Element of the carrier of G
(H * f) + (H * (- b)) is right_complementable Element of the carrier of G
the addF of G . ((H * f),(H * (- b))) is right_complementable Element of the carrier of G
G is non empty right_complementable almost_left_invertible add-associative right_zeroed unital associative commutative () () () () () () doubleLoopStr
the carrier of G is non empty set
0. G is V70(G) right_complementable Element of the carrier of G
the ZeroF of G is right_complementable Element of the carrier of G
H is right_complementable Element of the carrier of G
f is right_complementable Element of the carrier of G
H * f is right_complementable Element of the carrier of G
the multF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) associative Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the multF of G . (H,f) is right_complementable Element of the carrier of G
H " is right_complementable Element of the carrier of G
(H ") * (0. G) is right_complementable Element of the carrier of G
the multF of G . ((H "),(0. G)) is right_complementable Element of the carrier of G
(H ") * H is right_complementable Element of the carrier of G
the multF of G . ((H "),H) is right_complementable Element of the carrier of G
((H ") * H) * f is right_complementable Element of the carrier of G
the multF of G . (((H ") * H),f) is right_complementable Element of the carrier of G
1. G is right_complementable Element of the carrier of G
the OneF of G is right_complementable Element of the carrier of G
(1. G) * f is right_complementable Element of the carrier of G
the multF of G . ((1. G),f) is right_complementable Element of the carrier of G
G is non empty right_complementable add-associative right_zeroed () doubleLoopStr
the carrier of G is non empty set
H is right_complementable Element of the carrier of G
f is right_complementable Element of the carrier of G
H - f is right_complementable Element of the carrier of G
- f is right_complementable Element of the carrier of G
H + (- f) is right_complementable Element of the carrier of G
the addF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the addF of G . (H,(- f)) is right_complementable Element of the carrier of G
b is right_complementable Element of the carrier of G
(H - f) * b is right_complementable Element of the carrier of G
the multF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
the multF of G . ((H - f),b) is right_complementable Element of the carrier of G
H * b is right_complementable Element of the carrier of G
the multF of G . (H,b) is right_complementable Element of the carrier of G
f * b is right_complementable Element of the carrier of G
the multF of G . (f,b) is right_complementable Element of the carrier of G
(H * b) - (f * b) is right_complementable Element of the carrier of G
- (f * b) is right_complementable Element of the carrier of G
(H * b) + (- (f * b)) is right_complementable Element of the carrier of G
the addF of G . ((H * b),(- (f * b))) is right_complementable Element of the carrier of G
(- f) * b is right_complementable Element of the carrier of G
the multF of G . ((- f),b) is right_complementable Element of the carrier of G
(H * b) + ((- f) * b) is right_complementable Element of the carrier of G
the addF of G . ((H * b),((- f) * b)) is right_complementable Element of the carrier of G
G is 1-sorted
the non empty set is non empty set
[: the non empty set , the non empty set :] is set
[:[: the non empty set , the non empty set :], the non empty set :] is set
bool [:[: the non empty set , the non empty set :], the non empty set :] is set
the V1() V4([: the non empty set , the non empty set :]) V5( the non empty set ) Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :] is V1() V4([: the non empty set , the non empty set :]) V5( the non empty set ) Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :]
the Element of the non empty set is Element of the non empty set
the carrier of G is set
[: the carrier of G, the non empty set :] is set
[:[: the carrier of G, the non empty set :], the non empty set :] is set
bool [:[: the carrier of G, the non empty set :], the non empty set :] is set
the V1() V4([: the carrier of G, the non empty set :]) V5( the non empty set ) Function-like V18([: the carrier of G, the non empty set :], the non empty set ) Element of bool [:[: the carrier of G, the non empty set :], the non empty set :] is V1() V4([: the carrier of G, the non empty set :]) V5( the non empty set ) Function-like V18([: the carrier of G, the non empty set :], the non empty set ) Element of bool [:[: the carrier of G, the non empty set :], the non empty set :]
(G, the non empty set , the V1() V4([: the non empty set , the non empty set :]) V5( the non empty set ) Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Element of the non empty set , the V1() V4([: the carrier of G, the non empty set :]) V5( the non empty set ) Function-like V18([: the carrier of G, the non empty set :], the non empty set ) Element of bool [:[: the carrier of G, the non empty set :], the non empty set :]) is (G) (G)
the carrier of (G, the non empty set , the V1() V4([: the non empty set , the non empty set :]) V5( the non empty set ) Function-like V18([: the non empty set , the non empty set :], the non empty set ) Element of bool [:[: the non empty set , the non empty set :], the non empty set :], the Element of the non empty set , the V1() V4([: the carrier of G, the non empty set :]) V5( the non empty set ) Function-like V18([: the carrier of G, the non empty set :], the non empty set ) Element of bool [:[: the carrier of G, the non empty set :], the non empty set :]) is set
H is non empty set
[:H,H:] is set
[:[:H,H:],H:] is set
bool [:[:H,H:],H:] is set
G is 1-sorted
the carrier of G is set
[: the carrier of G,H:] is set
[:[: the carrier of G,H:],H:] is set
bool [:[: the carrier of G,H:],H:] is set
f is V1() V4([:H,H:]) V5(H) Function-like V18([:H,H:],H) Element of bool [:[:H,H:],H:]
b is Element of H
x is V1() V4([: the carrier of G,H:]) V5(H) Function-like V18([: the carrier of G,H:],H) Element of bool [:[: the carrier of G,H:],H:]
(G,H,f,b,x) is (G) (G)
G is 1-sorted
G is non empty 1-sorted
the carrier of G is non empty set
H is non empty (G)
the carrier of H is non empty set
the of H is V1() V4([: the carrier of G, the carrier of H:]) V5( the carrier of H) Function-like V18([: the carrier of G, the carrier of H:], the carrier of H) Element of bool [:[: the carrier of G, the carrier of H:], the carrier of H:]
[: the carrier of G, the carrier of H:] is set
[:[: the carrier of G, the carrier of H:], the carrier of H:] is set
bool [:[: the carrier of G, the carrier of H:], the carrier of H:] is set
f is Element of the carrier of G
b is Element of the carrier of H
the of H . (f,b) is Element of the carrier of H
G is non empty addLoopStr
the carrier of G is non empty set
[: the carrier of G, the carrier of G:] is set
bool [: the carrier of G, the carrier of G:] is set
H is V1() V4( the carrier of G) V5( the carrier of G) Function-like V18( the carrier of G, the carrier of G) Element of bool [: the carrier of G, the carrier of G:]
f is V1() V4( the carrier of G) V5( the carrier of G) Function-like V18( the carrier of G, the carrier of G) Element of bool [: the carrier of G, the carrier of G:]
b is set
H . b is set
x is Element of the carrier of G
- x is Element of the carrier of G
f . b is set
G is non empty right_complementable Abelian add-associative right_zeroed associative () () () () doubleLoopStr
the carrier of G is non empty set
[: the carrier of G, the carrier of G:] is set
[:[: the carrier of G, the carrier of G:], the carrier of G:] is set
bool [:[: the carrier of G, the carrier of G:], the carrier of G:] is set
the addF of G is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
0. G is V70(G) right_complementable Element of the carrier of G
the ZeroF of G is right_complementable Element of the carrier of G
H is V1() V4([: the carrier of G, the carrier of G:]) V5( the carrier of G) Function-like V18([: the carrier of G, the carrier of G:], the carrier of G) Element of bool [:[: the carrier of G, the carrier of G:], the carrier of G:]
(G, the carrier of G, the addF of G,(0. G),H) is non empty (G) (G)
the carrier of (G, the carrier of G, the addF of G,(0. G),H) is non empty set
b is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
x is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
b + x is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
the addF of (G, the carrier of G, the addF of G,(0. G),H) is V1() V4([: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):]) V5( the carrier of (G, the carrier of G, the addF of G,(0. G),H)) Function-like V18([: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):], the carrier of (G, the carrier of G, the addF of G,(0. G),H)) Element of bool [:[: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):], the carrier of (G, the carrier of G, the addF of G,(0. G),H):]
[: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):] is set
[:[: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):], the carrier of (G, the carrier of G, the addF of G,(0. G),H):] is set
bool [:[: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):], the carrier of (G, the carrier of G, the addF of G,(0. G),H):] is set
the addF of (G, the carrier of G, the addF of G,(0. G),H) . (b,x) is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
x + b is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
the addF of (G, the carrier of G, the addF of G,(0. G),H) . (x,b) is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
c8 is right_complementable Element of the carrier of G
y is right_complementable Element of the carrier of G
c8 + y is right_complementable Element of the carrier of G
the addF of G . (c8,y) is right_complementable Element of the carrier of G
the carrier of (G, the carrier of G, the addF of G,(0. G),H) is non empty set
b is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
x is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
b + x is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
the addF of (G, the carrier of G, the addF of G,(0. G),H) is V1() V4([: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):]) V5( the carrier of (G, the carrier of G, the addF of G,(0. G),H)) Function-like V18([: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):], the carrier of (G, the carrier of G, the addF of G,(0. G),H)) Element of bool [:[: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):], the carrier of (G, the carrier of G, the addF of G,(0. G),H):]
[: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):] is set
[:[: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):], the carrier of (G, the carrier of G, the addF of G,(0. G),H):] is set
bool [:[: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):], the carrier of (G, the carrier of G, the addF of G,(0. G),H):] is set
the addF of (G, the carrier of G, the addF of G,(0. G),H) . (b,x) is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
y is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
(b + x) + y is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
the addF of (G, the carrier of G, the addF of G,(0. G),H) . ((b + x),y) is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
x + y is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
the addF of (G, the carrier of G, the addF of G,(0. G),H) . (x,y) is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
b + (x + y) is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
the addF of (G, the carrier of G, the addF of G,(0. G),H) . (b,(x + y)) is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
c8 is right_complementable Element of the carrier of G
y is right_complementable Element of the carrier of G
c8 + y is right_complementable Element of the carrier of G
the addF of G . (c8,y) is right_complementable Element of the carrier of G
z is right_complementable Element of the carrier of G
(c8 + y) + z is right_complementable Element of the carrier of G
the addF of G . ((c8 + y),z) is right_complementable Element of the carrier of G
y + z is right_complementable Element of the carrier of G
the addF of G . (y,z) is right_complementable Element of the carrier of G
c8 + (y + z) is right_complementable Element of the carrier of G
the addF of G . (c8,(y + z)) is right_complementable Element of the carrier of G
the carrier of (G, the carrier of G, the addF of G,(0. G),H) is non empty set
b is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
0. (G, the carrier of G, the addF of G,(0. G),H) is V70((G, the carrier of G, the addF of G,(0. G),H)) Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
the ZeroF of (G, the carrier of G, the addF of G,(0. G),H) is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
b + (0. (G, the carrier of G, the addF of G,(0. G),H)) is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
the addF of (G, the carrier of G, the addF of G,(0. G),H) is V1() V4([: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):]) V5( the carrier of (G, the carrier of G, the addF of G,(0. G),H)) Function-like V18([: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):], the carrier of (G, the carrier of G, the addF of G,(0. G),H)) Element of bool [:[: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):], the carrier of (G, the carrier of G, the addF of G,(0. G),H):]
[: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):] is set
[:[: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):], the carrier of (G, the carrier of G, the addF of G,(0. G),H):] is set
bool [:[: the carrier of (G, the carrier of G, the addF of G,(0. G),H), the carrier of (G, the carrier of G, the addF of G,(0. G),H):], the carrier of (G, the carrier of G, the addF of G,(0. G),H):] is set
the addF of (G, the carrier of G, the addF of G,(0. G),H) . (b,(0. (G, the carrier of G, the addF of G,(0. G),H))) is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
x is right_complementable Element of the carrier of G
x + (0. G) is right_complementable Element of the carrier of G
the addF of G . (x,(0. G)) is right_complementable Element of the carrier of G
the carrier of (G, the carrier of G, the addF of G,(0. G),H) is non empty set
b is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
x is right_complementable Element of the carrier of G
y is right_complementable Element of the carrier of G
x + y is right_complementable Element of the carrier of G
the addF of G . (x,y) is right_complementable Element of the carrier of G
c8 is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
b + c8 is Element of the carrier of (G, the carrier of G, the addF of G,(0. G),H)
the addF of (G, the carrier of G, the addF of G,(