:: VECTSP_1 semantic presentation

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

c

y + c

the addF of G . (y,c

x is Element of the carrier of G

(y + c

the multF of G . ((y + c

y * x is Element of the carrier of G

the multF of G . (y,x) is Element of the carrier of G

c

the multF of G . (c

(y * x) + (c

the addF of G . ((y * x),(c

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

c

- c

- c

c

the addF of () . (c

c

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

c

c

c

the multF of () . (c

c

c

(c

the multF of () . ((c

(c

c

the multF of () . (c

c

c

the multF of () . (c

c

c

(1. ()) * c

the multF of () . ((1. ()),c

(1. ()) * c

c

c

c

c

c

the addF of () . (c

c

c

the multF of () . (c

c

c

the multF of () . (c

c

c

the multF of () . (c

c

(c

the addF of () . ((c

(c

c

c

c

the addF of () . (c

c

c

(c

the multF of () . ((c

(c

c

the multF of () . (c

c

c

the multF of () . (c

c

(c

the addF of () . ((c

(c

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

c

(y + z) * c

the multF of H . ((y + z),c

y * c

the multF of H . (y,c

z * c

the multF of H . (z,c

(y * c

the addF of H . ((y * c

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)

c

y is right_complementable Element of the carrier of G

c

the addF of G . (c

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)

c

y is right_complementable Element of the carrier of G

c

the addF of G . (c

z is right_complementable Element of the carrier of G

(c

the addF of G . ((c

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

c

the addF of G . (c

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

c

b + c

the addF of (G, the carrier of G, the addF of G,(