:: MATHMORP semantic presentation

REAL is V134() V135() V136() V140() set

NAT is V134() V135() V136() V137() V138() V139() V140() Element of K32(REAL)

K32(REAL) is set

omega is V134() V135() V136() V137() V138() V139() V140() set

K32(omega) is set

1 is non empty natural V24() real ext-real positive non negative V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT

K33(1,1) is set

K32(K33(1,1)) is set

K33(K33(1,1),1) is set

K32(K33(K33(1,1),1)) is set

K33(K33(1,1),REAL) is set

K32(K33(K33(1,1),REAL)) is set

K33(REAL,REAL) is set

K33(K33(REAL,REAL),REAL) is set

K32(K33(K33(REAL,REAL),REAL)) is set

2 is non empty natural V24() real ext-real positive non negative V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT

K33(2,2) is set

K33(K33(2,2),REAL) is set

K32(K33(K33(2,2),REAL)) is set

K32(NAT) is set

COMPLEX is V134() V140() set

RAT is V134() V135() V136() V137() V140() set

INT is V134() V135() V136() V137() V138() V140() set

K32(K33(REAL,REAL)) is set

TOP-REAL 2 is non empty TopSpace-like left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V153() strict RLTopStruct

the carrier of (TOP-REAL 2) is non empty set

K33(COMPLEX,COMPLEX) is set

K32(K33(COMPLEX,COMPLEX)) is set

K33(K33(COMPLEX,COMPLEX),COMPLEX) is set

K32(K33(K33(COMPLEX,COMPLEX),COMPLEX)) is set

K33(RAT,RAT) is set

K32(K33(RAT,RAT)) is set

K33(K33(RAT,RAT),RAT) is set

K32(K33(K33(RAT,RAT),RAT)) is set

K33(INT,INT) is set

K32(K33(INT,INT)) is set

K33(K33(INT,INT),INT) is set

K32(K33(K33(INT,INT),INT)) is set

K33(NAT,NAT) is set

K33(K33(NAT,NAT),NAT) is set

K32(K33(K33(NAT,NAT),NAT)) is set

K33(NAT,REAL) is set

K32(K33(NAT,REAL)) is set

{} is empty V134() V135() V136() V137() V138() V139() V140() set

the empty V134() V135() V136() V137() V138() V139() V140() set is empty V134() V135() V136() V137() V138() V139() V140() set

0 is empty natural V24() real ext-real non positive non negative V86() V87() V134() V135() V136() V137() V138() V139() V140() Element of NAT

t is non empty addMagma

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of the carrier of t

n is Element of K32( the carrier of t)

{ (b

B is set

x is Element of the carrier of t

x + s is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,x,s) is Element of the carrier of t

t is non empty addLoopStr

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

{ (- b

n is set

B is Element of the carrier of t

- B is Element of the carrier of t

t is non empty addMagma

the carrier of t is non empty set

K32( the carrier of t) is set

n is Element of K32( the carrier of t)

s is Element of K32( the carrier of t)

{ b

B is set

x is Element of the carrier of t

(t,x,n) is Element of K32( the carrier of t)

{ (b

t is non empty addLoopStr

the carrier of t is non empty set

K32( the carrier of t) is set

t is non empty right_complementable add-associative right_zeroed RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

(t,s) is Element of K32( the carrier of t)

{ (- b

(t,(t,s)) is Element of K32( the carrier of t)

{ (- b

n is set

B is Element of the carrier of t

- B is Element of the carrier of t

x is Element of the carrier of t

- x is Element of the carrier of t

n is set

B is Element of the carrier of t

- B is Element of the carrier of t

- (- B) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

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

{(0. t)} is non empty Element of K32( the carrier of t)

K32( the carrier of t) is set

s is Element of the carrier of t

(t,s,{(0. t)}) is Element of K32( the carrier of t)

{ (b

{s} is non empty Element of K32( the carrier of t)

n is set

B is Element of the carrier of t

B + s is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,B,s) is Element of the carrier of t

{B} is non empty Element of K32( the carrier of t)

{n} is non empty set

n is set

{n} is non empty set

(0. t) + s is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,(0. t),s) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

B is Element of the carrier of t

(t,B,s) is Element of K32( the carrier of t)

{ (b

(t,B,n) is Element of K32( the carrier of t)

{ (b

x is set

s1 is Element of the carrier of t

s1 + B is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,B) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of the carrier of t

n is Element of K32( the carrier of t)

(t,s,n) is Element of K32( the carrier of t)

{ (b

B is set

x is Element of the carrier of t

x + s is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,x,s) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

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

{(0. t)} is non empty Element of K32( the carrier of t)

s is Element of K32( the carrier of t)

(t,s,{(0. t)}) is Element of K32( the carrier of t)

{ b

n is set

{n} is non empty set

B is Element of the carrier of t

(t,B,{(0. t)}) is Element of K32( the carrier of t)

{ (b

n is set

{n} is non empty set

B is Element of the carrier of t

(t,B,{(0. t)}) is Element of K32( the carrier of t)

{ (b

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

s is Element of the carrier of t

{s} is non empty Element of K32( the carrier of t)

K32( the carrier of t) is set

n is Element of the carrier of t

(t,n,{s}) is Element of K32( the carrier of t)

{ (b

{n} is non empty Element of K32( the carrier of t)

(t,s,{n}) is Element of K32( the carrier of t)

{ (b

B is set

x is Element of the carrier of t

x + n is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,x,n) is Element of the carrier of t

{x} is non empty Element of K32( the carrier of t)

s + n is Element of the carrier of t

K164( the carrier of t, the addF of t,s,n) is Element of the carrier of t

B is set

x is Element of the carrier of t

x + s is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,x,s) is Element of the carrier of t

{x} is non empty Element of K32( the carrier of t)

s + n is Element of the carrier of t

K164( the carrier of t, the addF of t,s,n) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

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

{(0. t)} is non empty Element of K32( the carrier of t)

s is Element of K32( the carrier of t)

s + {(0. t)} is Element of K32( the carrier of t)

{ (b

n is set

B is Element of the carrier of t

x is Element of the carrier of t

B + x is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,B,x) is Element of the carrier of t

{x} is non empty Element of K32( the carrier of t)

n is set

B is Element of the carrier of t

B + (0. t) is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,B,(0. t)) is Element of the carrier of t

{ (b

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of the carrier of t

{n} is non empty Element of K32( the carrier of t)

s + {n} is Element of K32( the carrier of t)

{ (b

(t,n,s) is Element of K32( the carrier of t)

{ (b

B is set

x is Element of the carrier of t

s1 is Element of the carrier of t

x + s1 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,x,s1) is Element of the carrier of t

{s1} is non empty Element of K32( the carrier of t)

x + n is Element of the carrier of t

K164( the carrier of t, the addF of t,x,n) is Element of the carrier of t

B is set

x is Element of the carrier of t

x + n is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,x,n) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

(t,s,n) is Element of K32( the carrier of t)

{ b

B is set

x is Element of the carrier of t

(t,x,n) is Element of K32( the carrier of t)

{ (b

B is set

x is Element of the carrier of t

(t,x,n) is Element of K32( the carrier of t)

{ (b

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

B is Element of K32( the carrier of t)

(t,s,B) is Element of K32( the carrier of t)

{ b

(t,n,B) is Element of K32( the carrier of t)

{ b

s + B is Element of K32( the carrier of t)

{ (b

n + B is Element of K32( the carrier of t)

{ (b

x is set

s1 is Element of the carrier of t

(t,s1,B) is Element of K32( the carrier of t)

{ (b

x is set

s1 is Element of the carrier of t

s2 is Element of the carrier of t

s1 + s2 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,s2) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

B is Element of K32( the carrier of t)

(t,B,n) is Element of K32( the carrier of t)

{ b

(t,B,s) is Element of K32( the carrier of t)

{ b

B + s is Element of K32( the carrier of t)

{ (b

B + n is Element of K32( the carrier of t)

{ (b

x is set

s1 is Element of the carrier of t

(t,s1,n) is Element of K32( the carrier of t)

{ (b

(t,s1,s) is Element of K32( the carrier of t)

{ (b

x is set

s1 is Element of the carrier of t

s2 is Element of the carrier of t

s1 + s2 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,s2) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

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

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

(t,n,s) is Element of K32( the carrier of t)

{ b

n + s is Element of K32( the carrier of t)

{ (b

B is set

x is Element of the carrier of t

(t,x,s) is Element of K32( the carrier of t)

{ (b

(0. t) + x is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,(0. t),x) is Element of the carrier of t

{ (b

B is set

x is Element of the carrier of t

x + (0. t) is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,x,(0. t)) is Element of the carrier of t

{ (b

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

s + n is Element of K32( the carrier of t)

{ (b

n + s is Element of K32( the carrier of t)

{ (b

B is set

x is Element of the carrier of t

s1 is Element of the carrier of t

x + s1 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,x,s1) is Element of the carrier of t

B is set

x is Element of the carrier of t

s1 is Element of the carrier of t

x + s1 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,x,s1) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

s is Element of the carrier of t

n is Element of the carrier of t

s - n is Element of the carrier of t

- n is Element of the carrier of t

s + (- n) is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s,(- n)) is Element of the carrier of t

(s - n) + n is Element of the carrier of t

K164( the carrier of t, the addF of t,(s - n),n) is Element of the carrier of t

s + n is Element of the carrier of t

K164( the carrier of t, the addF of t,s,n) is Element of the carrier of t

(s + n) - n is Element of the carrier of t

(s + n) + (- n) is Element of the carrier of t

K164( the carrier of t, the addF of t,(s + n),(- n)) is Element of the carrier of t

n - n is Element of the carrier of t

n + (- n) is Element of the carrier of t

K164( the carrier of t, the addF of t,n,(- n)) is Element of the carrier of t

s + (n - n) is Element of the carrier of t

K164( the carrier of t, the addF of t,s,(n - n)) is Element of the carrier of t

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

s + (0. t) is Element of the carrier of t

K164( the carrier of t, the addF of t,s,(0. t)) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

B is Element of the carrier of t

(t,B,s) is Element of K32( the carrier of t)

{ (b

x is Element of the carrier of t

(t,x,n) is Element of K32( the carrier of t)

{ (b

B - x is Element of the carrier of t

- x is Element of the carrier of t

B + (- x) is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,B,(- x)) is Element of the carrier of t

(t,(B - x),s) is Element of K32( the carrier of t)

{ (b

s1 is set

s2 is Element of the carrier of t

s2 + (B - x) is Element of the carrier of t

K164( the carrier of t, the addF of t,s2,(B - x)) is Element of the carrier of t

b2 is Element of the carrier of t

s2 + B is Element of the carrier of t

K164( the carrier of t, the addF of t,s2,B) is Element of the carrier of t

(s2 + B) - x is Element of the carrier of t

(s2 + B) + (- x) is Element of the carrier of t

K164( the carrier of t, the addF of t,(s2 + B),(- x)) is Element of the carrier of t

b2 + x is Element of the carrier of t

K164( the carrier of t, the addF of t,b2,x) is Element of the carrier of t

{ (b

b1 is Element of the carrier of t

b1 + x is Element of the carrier of t

K164( the carrier of t, the addF of t,b1,x) is Element of the carrier of t

(b2 + x) - x is Element of the carrier of t

(b2 + x) + (- x) is Element of the carrier of t

K164( the carrier of t, the addF of t,(b2 + x),(- x)) is Element of the carrier of t

s1 is set

s2 is Element of the carrier of t

s2 + B is Element of the carrier of t

K164( the carrier of t, the addF of t,s2,B) is Element of the carrier of t

b2 is Element of the carrier of t

b2 - x is Element of the carrier of t

b2 + (- x) is Element of the carrier of t

K164( the carrier of t, the addF of t,b2,(- x)) is Element of the carrier of t

s2 + (B - x) is Element of the carrier of t

K164( the carrier of t, the addF of t,s2,(B - x)) is Element of the carrier of t

{ (b

(b2 - x) + x is Element of the carrier of t

K164( the carrier of t, the addF of t,(b2 - x),x) is Element of the carrier of t

{ (b

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

(t,s,n) is Element of K32( the carrier of t)

{ b

B is Element of the carrier of t

(t,B,s) is Element of K32( the carrier of t)

{ (b

(t,(t,B,s),n) is Element of K32( the carrier of t)

{ b

(t,B,(t,s,n)) is Element of K32( the carrier of t)

{ (b

x is set

s1 is Element of the carrier of t

(t,s1,n) is Element of K32( the carrier of t)

{ (b

s1 - B is Element of the carrier of t

- B is Element of the carrier of t

s1 + (- B) is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,(- B)) is Element of the carrier of t

(t,(s1 - B),n) is Element of K32( the carrier of t)

{ (b

(s1 - B) + B is Element of the carrier of t

K164( the carrier of t, the addF of t,(s1 - B),B) is Element of the carrier of t

{ (b

x is set

s1 is Element of the carrier of t

s1 + B is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,B) is Element of the carrier of t

s2 is Element of the carrier of t

s2 - B is Element of the carrier of t

- B is Element of the carrier of t

s2 + (- B) is Element of the carrier of t

K164( the carrier of t, the addF of t,s2,(- B)) is Element of the carrier of t

(t,s2,n) is Element of K32( the carrier of t)

{ (b

b2 is Element of the carrier of t

(t,b2,n) is Element of K32( the carrier of t)

{ (b

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

s + n is Element of K32( the carrier of t)

{ (b

B is Element of the carrier of t

(t,B,s) is Element of K32( the carrier of t)

{ (b

(t,B,s) + n is Element of K32( the carrier of t)

{ (b

(t,B,(s + n)) is Element of K32( the carrier of t)

{ (b

x is set

s1 is Element of the carrier of t

s2 is Element of the carrier of t

s1 + s2 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,s2) is Element of the carrier of t

b2 is Element of the carrier of t

b2 + B is Element of the carrier of t

K164( the carrier of t, the addF of t,b2,B) is Element of the carrier of t

b2 + s2 is Element of the carrier of t

K164( the carrier of t, the addF of t,b2,s2) is Element of the carrier of t

(b2 + s2) + B is Element of the carrier of t

K164( the carrier of t, the addF of t,(b2 + s2),B) is Element of the carrier of t

x is set

s1 is Element of the carrier of t

s1 + B is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,B) is Element of the carrier of t

s2 is Element of the carrier of t

b2 is Element of the carrier of t

s2 + b2 is Element of the carrier of t

K164( the carrier of t, the addF of t,s2,b2) is Element of the carrier of t

s2 + B is Element of the carrier of t

K164( the carrier of t, the addF of t,s2,B) is Element of the carrier of t

(s2 + B) + b2 is Element of the carrier of t

K164( the carrier of t, the addF of t,(s2 + B),b2) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of the carrier of t

(t,n,s) is Element of K32( the carrier of t)

{ (b

B is Element of the carrier of t

(t,B,(t,n,s)) is Element of K32( the carrier of t)

{ (b

n + B is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,n,B) is Element of the carrier of t

(t,(n + B),s) is Element of K32( the carrier of t)

{ (b

x is set

s1 is Element of the carrier of t

s1 + B is Element of the carrier of t

K164( the carrier of t, the addF of t,s1,B) is Element of the carrier of t

s2 is Element of the carrier of t

s2 + n is Element of the carrier of t

K164( the carrier of t, the addF of t,s2,n) is Element of the carrier of t

s2 + (n + B) is Element of the carrier of t

K164( the carrier of t, the addF of t,s2,(n + B)) is Element of the carrier of t

x is set

s1 is Element of the carrier of t

s1 + (n + B) is Element of the carrier of t

K164( the carrier of t, the addF of t,s1,(n + B)) is Element of the carrier of t

s1 + n is Element of the carrier of t

K164( the carrier of t, the addF of t,s1,n) is Element of the carrier of t

(s1 + n) + B is Element of the carrier of t

K164( the carrier of t, the addF of t,(s1 + n),B) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

(t,s,n) is Element of K32( the carrier of t)

{ b

B is Element of the carrier of t

(t,B,n) is Element of K32( the carrier of t)

{ (b

(t,s,(t,B,n)) is Element of K32( the carrier of t)

{ b

- B is Element of the carrier of t

(t,(- B),(t,s,n)) is Element of K32( the carrier of t)

{ (b

x is set

s1 is Element of the carrier of t

(t,s1,(t,B,n)) is Element of K32( the carrier of t)

{ (b

s1 + B is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,B) is Element of the carrier of t

(t,(s1 + B),n) is Element of K32( the carrier of t)

{ (b

(s1 + B) - B is Element of the carrier of t

(s1 + B) + (- B) is Element of the carrier of t

K164( the carrier of t, the addF of t,(s1 + B),(- B)) is Element of the carrier of t

x is set

s1 is Element of the carrier of t

s1 + (- B) is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,(- B)) is Element of the carrier of t

s2 is Element of the carrier of t

s2 + B is Element of the carrier of t

K164( the carrier of t, the addF of t,s2,B) is Element of the carrier of t

s1 - B is Element of the carrier of t

s1 + (- B) is Element of the carrier of t

(s1 - B) + B is Element of the carrier of t

K164( the carrier of t, the addF of t,(s1 - B),B) is Element of the carrier of t

(t,s2,(t,B,n)) is Element of K32( the carrier of t)

{ (b

b2 is Element of the carrier of t

(t,b2,n) is Element of K32( the carrier of t)

{ (b

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

s + n is Element of K32( the carrier of t)

{ (b

B is Element of the carrier of t

(t,B,n) is Element of K32( the carrier of t)

{ (b

s + (t,B,n) is Element of K32( the carrier of t)

{ (b

(t,B,(s + n)) is Element of K32( the carrier of t)

{ (b

x is set

s1 is Element of the carrier of t

s2 is Element of the carrier of t

s1 + s2 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,s2) is Element of the carrier of t

b2 is Element of the carrier of t

b2 + B is Element of the carrier of t

K164( the carrier of t, the addF of t,b2,B) is Element of the carrier of t

s1 + b2 is Element of the carrier of t

K164( the carrier of t, the addF of t,s1,b2) is Element of the carrier of t

(s1 + b2) + B is Element of the carrier of t

K164( the carrier of t, the addF of t,(s1 + b2),B) is Element of the carrier of t

x is set

s1 is Element of the carrier of t

s1 + B is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,B) is Element of the carrier of t

s2 is Element of the carrier of t

b2 is Element of the carrier of t

s2 + b2 is Element of the carrier of t

K164( the carrier of t, the addF of t,s2,b2) is Element of the carrier of t

b2 + B is Element of the carrier of t

K164( the carrier of t, the addF of t,b2,B) is Element of the carrier of t

s2 + (b2 + B) is Element of the carrier of t

K164( the carrier of t, the addF of t,s2,(b2 + B)) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

n + s is Element of K32( the carrier of t)

{ (b

B is Element of the carrier of t

(t,B,n) is Element of K32( the carrier of t)

{ (b

x is set

s1 is Element of the carrier of t

s1 + B is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,B) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

s + n is Element of K32( the carrier of t)

{ (b

(t,(s + n),n) is Element of K32( the carrier of t)

{ b

B is set

x is Element of the carrier of t

(t,x,n) is Element of K32( the carrier of t)

{ (b

n + s is Element of K32( the carrier of t)

{ (b

(t,(n + s),n) is Element of K32( the carrier of t)

{ b

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

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

s is Element of K32( the carrier of t)

(t,(0. t),s) is Element of K32( the carrier of t)

{ (b

n is set

B is Element of the carrier of t

B + (0. t) is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,B,(0. t)) is Element of the carrier of t

n is set

B is Element of the carrier of t

B + (0. t) is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,B,(0. t)) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of the carrier of t

{n} is non empty Element of K32( the carrier of t)

(t,s,{n}) is Element of K32( the carrier of t)

{ b

- n is Element of the carrier of t

(t,(- n),s) is Element of K32( the carrier of t)

{ (b

B is set

x is Element of the carrier of t

(t,x,{n}) is Element of K32( the carrier of t)

{ (b

{x} is non empty Element of K32( the carrier of t)

(t,n,{x}) is Element of K32( the carrier of t)

{ (b

(t,(- n),(t,n,{x})) is Element of K32( the carrier of t)

{ (b

n + (- n) is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,n,(- n)) is Element of the carrier of t

(t,(n + (- n)),{x}) is Element of K32( the carrier of t)

{ (b

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

(t,(0. t),{x}) is Element of K32( the carrier of t)

{ (b

B is set

x is Element of the carrier of t

x + (- n) is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,x,(- n)) is Element of the carrier of t

s1 is Element of the carrier of t

x - n is Element of the carrier of t

x + (- n) is Element of the carrier of t

s1 + n is Element of the carrier of t

K164( the carrier of t, the addF of t,s1,n) is Element of the carrier of t

(t,s1,{n}) is Element of K32( the carrier of t)

{ (b

s2 is set

b2 is Element of the carrier of t

b2 + s1 is Element of the carrier of t

K164( the carrier of t, the addF of t,b2,s1) is Element of the carrier of t

{b2} is non empty Element of K32( the carrier of t)

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

(t,s,n) is Element of K32( the carrier of t)

{ b

(t,s,n) + n is Element of K32( the carrier of t)

{ (b

B is set

x is Element of the carrier of t

s1 is Element of the carrier of t

x + s1 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,x,s1) is Element of the carrier of t

s2 is Element of the carrier of t

(t,s2,n) is Element of K32( the carrier of t)

{ (b

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

(t,s,n) is Element of K32( the carrier of t)

{ b

B is Element of K32( the carrier of t)

n + B is Element of K32( the carrier of t)

{ (b

(t,s,(n + B)) is Element of K32( the carrier of t)

{ b

(t,(t,s,n),B) is Element of K32( the carrier of t)

{ b

(t,s,n) + n is Element of K32( the carrier of t)

{ (b

x is set

s1 is Element of the carrier of t

(t,s1,(n + B)) is Element of K32( the carrier of t)

{ (b

(t,s1,n) is Element of K32( the carrier of t)

{ (b

(t,s1,n) + B is Element of K32( the carrier of t)

{ (b

B + (t,s1,n) is Element of K32( the carrier of t)

{ (b

(t,(B + (t,s1,n)),(t,s1,n)) is Element of K32( the carrier of t)

{ b

(t,s,(t,s1,n)) is Element of K32( the carrier of t)

{ b

- s1 is Element of the carrier of t

(t,(- s1),(t,s,n)) is Element of K32( the carrier of t)

{ (b

(t,s1,B) is Element of K32( the carrier of t)

{ (b

(t,s1,(t,(- s1),(t,s,n))) is Element of K32( the carrier of t)

{ (b

(- s1) + s1 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,(- s1),s1) is Element of the carrier of t

(t,((- s1) + s1),(t,s,n)) is Element of K32( the carrier of t)

{ (b

s1 - s1 is Element of the carrier of t

s1 + (- s1) is Element of the carrier of t

K164( the carrier of t, the addF of t,s1,(- s1)) is Element of the carrier of t

(t,(s1 - s1),(t,s,n)) is Element of K32( the carrier of t)

{ (b

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

(t,(0. t),(t,s,n)) is Element of K32( the carrier of t)

{ (b

x is set

s1 is Element of the carrier of t

(t,s1,B) is Element of K32( the carrier of t)

{ (b

(t,s1,B) + n is Element of K32( the carrier of t)

{ (b

B + n is Element of K32( the carrier of t)

{ (b

(t,s1,(B + n)) is Element of K32( the carrier of t)

{ (b

(t,s,(B + n)) is Element of K32( the carrier of t)

{ b

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

B is Element of K32( the carrier of t)

n + B is Element of K32( the carrier of t)

{ (b

(t,s,(n + B)) is Element of K32( the carrier of t)

{ b

(t,s,B) is Element of K32( the carrier of t)

{ b

(t,(t,s,B),n) is Element of K32( the carrier of t)

{ b

B + n is Element of K32( the carrier of t)

{ (b

(t,s,(B + n)) is Element of K32( the carrier of t)

{ b

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

s + n is Element of K32( the carrier of t)

{ (b

B is Element of K32( the carrier of t)

(t,n,B) is Element of K32( the carrier of t)

{ b

s + (t,n,B) is Element of K32( the carrier of t)

{ (b

(t,(s + n),B) is Element of K32( the carrier of t)

{ b

x is set

s1 is Element of the carrier of t

s2 is Element of the carrier of t

s1 + s2 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,s2) is Element of the carrier of t

(t,s2,B) is Element of K32( the carrier of t)

{ (b

(t,s1,(t,s2,B)) is Element of K32( the carrier of t)

{ (b

(t,s1,n) is Element of K32( the carrier of t)

{ (b

b2 is Element of the carrier of t

(t,b2,B) is Element of K32( the carrier of t)

{ (b

s2 + s1 is Element of the carrier of t

K164( the carrier of t, the addF of t,s2,s1) is Element of the carrier of t

(t,(s2 + s1),B) is Element of K32( the carrier of t)

{ (b

n + s is Element of K32( the carrier of t)

{ (b

(t,(n + s),B) is Element of K32( the carrier of t)

{ b

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

s + n is Element of K32( the carrier of t)

{ (b

B is Element of K32( the carrier of t)

n + B is Element of K32( the carrier of t)

{ (b

s + (n + B) is Element of K32( the carrier of t)

{ (b

(s + n) + B is Element of K32( the carrier of t)

{ (b

x is set

s1 is Element of the carrier of t

s2 is Element of the carrier of t

s1 + s2 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,s2) is Element of the carrier of t

b2 is Element of the carrier of t

b1 is Element of the carrier of t

b2 + b1 is Element of the carrier of t

K164( the carrier of t, the addF of t,b2,b1) is Element of the carrier of t

s1 + b2 is Element of the carrier of t

K164( the carrier of t, the addF of t,s1,b2) is Element of the carrier of t

(s1 + b2) + b1 is Element of the carrier of t

K164( the carrier of t, the addF of t,(s1 + b2),b1) is Element of the carrier of t

x is set

s1 is Element of the carrier of t

s2 is Element of the carrier of t

s1 + s2 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,s2) is Element of the carrier of t

b2 is Element of the carrier of t

b1 is Element of the carrier of t

b2 + b1 is Element of the carrier of t

K164( the carrier of t, the addF of t,b2,b1) is Element of the carrier of t

b1 + s2 is Element of the carrier of t

K164( the carrier of t, the addF of t,b1,s2) is Element of the carrier of t

b2 + (b1 + s2) is Element of the carrier of t

K164( the carrier of t, the addF of t,b2,(b1 + s2)) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

s \/ n is Element of K32( the carrier of t)

B is Element of the carrier of t

(t,B,(s \/ n)) is Element of K32( the carrier of t)

{ (b

(t,B,s) is Element of K32( the carrier of t)

{ (b

(t,B,n) is Element of K32( the carrier of t)

{ (b

(t,B,s) \/ (t,B,n) is Element of K32( the carrier of t)

x is set

s1 is Element of the carrier of t

s1 + B is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,B) is Element of the carrier of t

{ (b

{ (b

x is set

s1 is Element of the carrier of t

s1 + B is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,B) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

s /\ n is Element of K32( the carrier of t)

B is Element of the carrier of t

(t,B,(s /\ n)) is Element of K32( the carrier of t)

{ (b

(t,B,s) is Element of K32( the carrier of t)

{ (b

(t,B,n) is Element of K32( the carrier of t)

{ (b

(t,B,s) /\ (t,B,n) is Element of K32( the carrier of t)

x is set

s1 is Element of the carrier of t

s1 + B is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,B) is Element of the carrier of t

{ (b

{ (b

x is set

s1 is Element of the carrier of t

s1 + B is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,B) is Element of the carrier of t

s2 is Element of the carrier of t

s2 + B is Element of the carrier of t

K164( the carrier of t, the addF of t,s2,B) is Element of the carrier of t

(s2 + B) - B is Element of the carrier of t

- B is Element of the carrier of t

(s2 + B) + (- B) is Element of the carrier of t

K164( the carrier of t, the addF of t,(s2 + B),(- B)) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

(t,s,n) is Element of K32( the carrier of t)

{ b

B is Element of K32( the carrier of t)

n \/ B is Element of K32( the carrier of t)

(t,s,(n \/ B)) is Element of K32( the carrier of t)

{ b

(t,s,B) is Element of K32( the carrier of t)

{ b

(t,s,n) /\ (t,s,B) is Element of K32( the carrier of t)

x is set

s1 is Element of the carrier of t

(t,s1,(n \/ B)) is Element of K32( the carrier of t)

{ (b

(t,s1,n) is Element of K32( the carrier of t)

{ (b

(t,s1,B) is Element of K32( the carrier of t)

{ (b

(t,s1,n) \/ (t,s1,B) is Element of K32( the carrier of t)

x is set

s1 is Element of the carrier of t

(t,s1,n) is Element of K32( the carrier of t)

{ (b

(t,s1,B) is Element of K32( the carrier of t)

{ (b

(t,s1,n) \/ (t,s1,B) is Element of K32( the carrier of t)

s2 is Element of the carrier of t

(t,s2,B) is Element of K32( the carrier of t)

{ (b

(t,s1,(n \/ B)) is Element of K32( the carrier of t)

{ (b

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

s + n is Element of K32( the carrier of t)

{ (b

B is Element of K32( the carrier of t)

n \/ B is Element of K32( the carrier of t)

s + (n \/ B) is Element of K32( the carrier of t)

{ (b

s + B is Element of K32( the carrier of t)

{ (b

(s + n) \/ (s + B) is Element of K32( the carrier of t)

x is set

s1 is Element of the carrier of t

s2 is Element of the carrier of t

s1 + s2 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,s2) is Element of the carrier of t

{ (b

{ (b

x is set

s1 is Element of the carrier of t

s2 is Element of the carrier of t

s1 + s2 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,s2) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

(t,s,n) is Element of K32( the carrier of t)

{ b

B is Element of K32( the carrier of t)

(t,B,n) is Element of K32( the carrier of t)

{ b

(t,s,n) \/ (t,B,n) is Element of K32( the carrier of t)

s \/ B is Element of K32( the carrier of t)

(t,(s \/ B),n) is Element of K32( the carrier of t)

{ b

x is set

s1 is Element of the carrier of t

(t,s1,n) is Element of K32( the carrier of t)

{ (b

s2 is set

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

s \/ n is Element of K32( the carrier of t)

B is Element of K32( the carrier of t)

(s \/ n) + B is Element of K32( the carrier of t)

{ (b

s + B is Element of K32( the carrier of t)

{ (b

n + B is Element of K32( the carrier of t)

{ (b

(s + B) \/ (n + B) is Element of K32( the carrier of t)

x is set

s1 is Element of the carrier of t

s2 is Element of the carrier of t

s1 + s2 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,s2) is Element of the carrier of t

{ (b

{ (b

x is set

s1 is Element of the carrier of t

s2 is Element of the carrier of t

s1 + s2 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,s2) is Element of the carrier of t

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

s /\ n is Element of K32( the carrier of t)

B is Element of K32( the carrier of t)

(t,(s /\ n),B) is Element of K32( the carrier of t)

{ b

(t,s,B) is Element of K32( the carrier of t)

{ b

(t,n,B) is Element of K32( the carrier of t)

{ b

(t,s,B) /\ (t,n,B) is Element of K32( the carrier of t)

x is set

s1 is Element of the carrier of t

(t,s1,B) is Element of K32( the carrier of t)

{ (b

x is set

s1 is Element of the carrier of t

(t,s1,B) is Element of K32( the carrier of t)

{ (b

s2 is set

b2 is Element of the carrier of t

(t,b2,B) is Element of K32( the carrier of t)

{ (b

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

s /\ n is Element of K32( the carrier of t)

B is Element of K32( the carrier of t)

(s /\ n) + B is Element of K32( the carrier of t)

{ (b

s + B is Element of K32( the carrier of t)

{ (b

n + B is Element of K32( the carrier of t)

{ (b

(s + B) /\ (n + B) is Element of K32( the carrier of t)

x is set

s1 is Element of the carrier of t

s2 is Element of the carrier of t

s1 + s2 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,s1,s2) is Element of the carrier of t

{ (b

{ (b

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

s + n is Element of K32( the carrier of t)

{ (b

B is Element of K32( the carrier of t)

n /\ B is Element of K32( the carrier of t)

s + (n /\ B) is Element of K32( the carrier of t)

{ (b

s + B is Element of K32( the carrier of t)

{ (b

(s + n) /\ (s + B) is Element of K32( the carrier of t)

(n /\ B) + s is Element of K32( the carrier of t)

{ (b

n + s is Element of K32( the carrier of t)

{ (b

B + s is Element of K32( the carrier of t)

{ (b

(n + s) /\ (B + s) is Element of K32( the carrier of t)

(s + n) /\ (B + s) is Element of K32( the carrier of t)

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

n is Element of K32( the carrier of t)

(t,s,n) is Element of K32( the carrier of t)

{ b

B is Element of K32( the carrier of t)

(t,s,B) is Element of K32( the carrier of t)

{ b

(t,s,n) \/ (t,s,B) is Element of K32( the carrier of t)

n /\ B is Element of K32( the carrier of t)

(t,s,(n /\ B)) is Element of K32( the carrier of t)

{ b

x is set

s1 is Element of the carrier of t

(t,s1,n) is Element of K32( the carrier of t)

{ (b

(t,s1,B) is Element of K32( the carrier of t)

{ (b

(t,s1,n) /\ (t,s1,B) is Element of K32( the carrier of t)

s2 is set

(t,s1,(n /\ B)) is Element of K32( the carrier of t)

{ (b

t is non empty left_complementable right_complementable Abelian add-associative right_zeroed V153() RLSStruct

the carrier of t is non empty set

K32( the carrier of t) is set

s is Element of K32( the carrier of t)

s ` is Element of K32( the carrier of t)

the carrier of t \ s is set

n is Element of K32( the carrier of t)

(t,(s `),n) is Element of K32( the carrier of t)

{ b

(t,(s `),n) ` is Element of K32( the carrier of t)

the carrier of t \ (t,(s `),n) is set

(t,n) is Element of K32( the carrier of t)

{ (- b

s + (t,n) is Element of K32( the carrier of t)

{ (b

B is set

x is Element of the carrier of t

(t,x,n) is Element of K32( the carrier of t)

{ (b

s1 is set

b2 is Element of the carrier of t

b2 + x is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the carrier of t, the carrier of t) is set

K33(K33( the carrier of t, the carrier of t), the carrier of t) is set

K32(K33(K33( the carrier of t, the carrier of t), the carrier of t)) is set

K164( the carrier of t, the addF of t,b2,x) is Element of the carrier of t

s2 is Element of the carrier of t

s2 - b2 is Element of the carrier of t

- b2 is Element of the carrier of t

s2 + (- b2) is Element of the carrier of t

K164( the carrier of t, the addF of t,s2,(- b2)) is Element of the carrier of t

B is set

x is Element of the carrier of t

s1 is Element of the carrier of t

x + s1 is Element of the carrier of t

the addF of t is V12() V30(K33( the carrier of t, the carrier of t), the carrier of t) Element of K32(K33(K33( the carrier of t, the carrier of t), the carrier of t))

K33( the