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

the carrier of () 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
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)
{ (b1 + s) where b1 is Element of the carrier of t : b1 in n } is set
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
the carrier of t is non empty set
K32( the carrier of t) is set
s is Element of K32( the carrier of t)
{ (- b1) where b1 is Element of the carrier of t : b1 in s } is set
n is set
B is Element of the carrier of t
- B is Element of the carrier of t
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)
{ b1 where b1 is Element of the carrier of t : (t,b1,n) c= s } is set
B is set
x is Element of the carrier of t
(t,x,n) is Element of K32( the carrier of t)
{ (b1 + x) where b1 is Element of the carrier of t : b1 in n } is set
the carrier of t is non empty set
K32( the carrier of t) is set

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)
{ (- b1) where b1 is Element of the carrier of t : b1 in s } is set
(t,(t,s)) is Element of K32( the carrier of t)
{ (- b1) where b1 is Element of the carrier of t : b1 in (t,s) } is set
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

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)
{ (b1 + s) where b1 is Element of the carrier of t : b1 in {(0. t)} } is set
{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

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)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in s } is set
(t,B,n) is Element of K32( the carrier of t)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in n } is set
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

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)
{ (b1 + s) where b1 is Element of the carrier of t : b1 in n } is set
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

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)
{ b1 where b1 is Element of the carrier of t : (t,b1,{(0. t)}) c= s } is set
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)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in {(0. t)} } is set
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)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in {(0. t)} } is set

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)
{ (b1 + n) where b1 is Element of the carrier of t : b1 in {s} } is set
{n} is non empty Element of K32( the carrier of t)
(t,s,{n}) is Element of K32( the carrier of t)
{ (b1 + s) where b1 is Element of the carrier of t : b1 in {n} } is set
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

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)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in {(0. t)} ) } is set
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
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in {(0. t)} ) } is set

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)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in {n} ) } is set
(t,n,s) is Element of K32( the carrier of t)
{ (b1 + n) where b1 is Element of the carrier of t : b1 in s } is set
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

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)
{ b1 where b1 is Element of the carrier of t : (t,b1,n) c= s } is set
B is set
x is Element of the carrier of t
(t,x,n) is Element of K32( the carrier of t)
{ (b1 + x) where b1 is Element of the carrier of t : b1 in n } is set
B is set
x is Element of the carrier of t
(t,x,n) is Element of K32( the carrier of t)
{ (b1 + x) where b1 is Element of the carrier of t : b1 in n } is set

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)
{ b1 where b1 is Element of the carrier of t : (t,b1,B) c= s } is set
(t,n,B) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,B) c= n } is set
s + B is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in B ) } is set
n + B is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in n & b2 in B ) } is set
x is set
s1 is Element of the carrier of t
(t,s1,B) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in B } is set
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

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)
{ b1 where b1 is Element of the carrier of t : (t,b1,n) c= B } is set
(t,B,s) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,s) c= B } is set
B + s is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in B & b2 in s ) } is set
B + n is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in B & b2 in n ) } is set
x is set
s1 is Element of the carrier of t
(t,s1,n) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in n } is set
(t,s1,s) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in s } is set
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

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)
{ b1 where b1 is Element of the carrier of t : (t,b1,s) c= n } is set
n + s is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in n & b2 in s ) } is set
B is set
x is Element of the carrier of t
(t,x,s) is Element of K32( the carrier of t)
{ (b1 + x) where b1 is Element of the carrier of t : b1 in s } is set
(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
{ (b1 + x) where b1 is Element of the carrier of t : b1 in s } is set
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
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in n & b2 in s ) } is set

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)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in n ) } is set
n + s is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in n & b2 in s ) } is set
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

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

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)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in s } is set
x is Element of the carrier of t
(t,x,n) is Element of K32( the carrier of t)
{ (b1 + x) where b1 is Element of the carrier of t : b1 in n } is set
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)
{ (b1 + (B - x)) where b1 is Element of the carrier of t : b1 in s } is set
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
{ (b1 + B) where b1 is Element of the carrier of t : b1 in s } is set
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
{ (b1 + (B - x)) where b1 is Element of the carrier of t : b1 in s } is set
(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
{ (b1 + x) where b1 is Element of the carrier of t : b1 in n } is set

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)
{ b1 where b1 is Element of the carrier of t : (t,b1,n) c= s } is set
B is Element of the carrier of t
(t,B,s) is Element of K32( the carrier of t)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in s } is set
(t,(t,B,s),n) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,n) c= (t,B,s) } is set
(t,B,(t,s,n)) is Element of K32( the carrier of t)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in (t,s,n) } is set
x is set
s1 is Element of the carrier of t
(t,s1,n) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in n } is set
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)
{ (b1 + (s1 - B)) where b1 is Element of the carrier of t : b1 in n } is set
(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
{ (b1 + B) where b1 is Element of the carrier of t : b1 in (t,s,n) } is set
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)
{ (b1 + s2) where b1 is Element of the carrier of t : b1 in n } is set
b2 is Element of the carrier of t
(t,b2,n) is Element of K32( the carrier of t)
{ (b1 + b2) where b1 is Element of the carrier of t : b1 in n } is set

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)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in n ) } is set
B is Element of the carrier of t
(t,B,s) is Element of K32( the carrier of t)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in s } is set
(t,B,s) + n is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in (t,B,s) & b2 in n ) } is set
(t,B,(s + n)) is Element of K32( the carrier of t)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in s + n } is set
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

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)
{ (b1 + n) where b1 is Element of the carrier of t : b1 in s } is set
B is Element of the carrier of t
(t,B,(t,n,s)) is Element of K32( the carrier of t)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in (t,n,s) } is set
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)
{ (b1 + (n + B)) where b1 is Element of the carrier of t : b1 in s } is set
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

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)
{ b1 where b1 is Element of the carrier of t : (t,b1,n) c= s } is set
B is Element of the carrier of t
(t,B,n) is Element of K32( the carrier of t)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in n } is set
(t,s,(t,B,n)) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,(t,B,n)) c= s } is set
- B is Element of the carrier of t
(t,(- B),(t,s,n)) is Element of K32( the carrier of t)
{ (b1 + (- B)) where b1 is Element of the carrier of t : b1 in (t,s,n) } is set
x is set
s1 is Element of the carrier of t
(t,s1,(t,B,n)) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in (t,B,n) } is set
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)
{ (b1 + (s1 + B)) where b1 is Element of the carrier of t : b1 in n } is set
(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)
{ (b1 + s2) where b1 is Element of the carrier of t : b1 in (t,B,n) } is set
b2 is Element of the carrier of t
(t,b2,n) is Element of K32( the carrier of t)
{ (b1 + b2) where b1 is Element of the carrier of t : b1 in n } is set

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)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in n ) } is set
B is Element of the carrier of t
(t,B,n) is Element of K32( the carrier of t)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in n } is set
s + (t,B,n) is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in (t,B,n) ) } is set
(t,B,(s + n)) is Element of K32( the carrier of t)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in s + n } is set
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

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)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in n & b2 in s ) } is set
B is Element of the carrier of t
(t,B,n) is Element of K32( the carrier of t)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in n } is set
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

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)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in n ) } is set
(t,(s + n),n) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,n) c= s + n } is set
B is set
x is Element of the carrier of t
(t,x,n) is Element of K32( the carrier of t)
{ (b1 + x) where b1 is Element of the carrier of t : b1 in n } is set
n + s is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in n & b2 in s ) } is set
(t,(n + s),n) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,n) c= n + s } is set

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)
{ (b1 + (0. t)) where b1 is Element of the carrier of t : b1 in s } is set
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

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)
{ b1 where b1 is Element of the carrier of t : (t,b1,{n}) c= s } is set
- n is Element of the carrier of t
(t,(- n),s) is Element of K32( the carrier of t)
{ (b1 + (- n)) where b1 is Element of the carrier of t : b1 in s } is set
B is set
x is Element of the carrier of t
(t,x,{n}) is Element of K32( the carrier of t)
{ (b1 + x) where b1 is Element of the carrier of t : b1 in {n} } is set
{x} is non empty Element of K32( the carrier of t)
(t,n,{x}) is Element of K32( the carrier of t)
{ (b1 + n) where b1 is Element of the carrier of t : b1 in {x} } is set
(t,(- n),(t,n,{x})) is Element of K32( the carrier of t)
{ (b1 + (- n)) where b1 is Element of the carrier of t : b1 in (t,n,{x}) } is set
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)
{ (b1 + (n + (- n))) where b1 is Element of the carrier of t : b1 in {x} } is set
0. t is V49(t) Element of the carrier of t
(t,(0. t),{x}) is Element of K32( the carrier of t)
{ (b1 + (0. t)) where b1 is Element of the carrier of t : b1 in {x} } is set
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)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in {n} } is set
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)

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)
{ b1 where b1 is Element of the carrier of t : (t,b1,n) c= s } is set
(t,s,n) + n is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in (t,s,n) & b2 in n ) } is set
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)
{ (b1 + s2) where b1 is Element of the carrier of t : b1 in n } is set

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)
{ b1 where b1 is Element of the carrier of t : (t,b1,n) c= s } is set
B is Element of K32( the carrier of t)
n + B is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in n & b2 in B ) } is set
(t,s,(n + B)) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,(n + B)) c= s } is set
(t,(t,s,n),B) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,B) c= (t,s,n) } is set
(t,s,n) + n is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in (t,s,n) & b2 in n ) } is set
x is set
s1 is Element of the carrier of t
(t,s1,(n + B)) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in n + B } is set
(t,s1,n) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in n } is set
(t,s1,n) + B is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in (t,s1,n) & b2 in B ) } is set
B + (t,s1,n) is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in B & b2 in (t,s1,n) ) } is set
(t,(B + (t,s1,n)),(t,s1,n)) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,(t,s1,n)) c= B + (t,s1,n) } is set
(t,s,(t,s1,n)) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,(t,s1,n)) c= s } is set
- s1 is Element of the carrier of t
(t,(- s1),(t,s,n)) is Element of K32( the carrier of t)
{ (b1 + (- s1)) where b1 is Element of the carrier of t : b1 in (t,s,n) } is set
(t,s1,B) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in B } is set
(t,s1,(t,(- s1),(t,s,n))) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in (t,(- s1),(t,s,n)) } is set
(- 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)
{ (b1 + ((- s1) + s1)) where b1 is Element of the carrier of t : b1 in (t,s,n) } is set
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)
{ (b1 + (s1 - s1)) where b1 is Element of the carrier of t : b1 in (t,s,n) } is set
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)
{ (b1 + (0. t)) where b1 is Element of the carrier of t : b1 in (t,s,n) } is set
x is set
s1 is Element of the carrier of t
(t,s1,B) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in B } is set
(t,s1,B) + n is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in (t,s1,B) & b2 in n ) } is set
B + n is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in B & b2 in n ) } is set
(t,s1,(B + n)) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in B + n } is set
(t,s,(B + n)) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,(B + n)) c= s } is set

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)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in n & b2 in B ) } is set
(t,s,(n + B)) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,(n + B)) c= s } is set
(t,s,B) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,B) c= s } is set
(t,(t,s,B),n) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,n) c= (t,s,B) } is set
B + n is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in B & b2 in n ) } is set
(t,s,(B + n)) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,(B + n)) c= s } is set

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)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in n ) } is set
B is Element of K32( the carrier of t)
(t,n,B) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,B) c= n } is set
s + (t,n,B) is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in (t,n,B) ) } is set
(t,(s + n),B) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,B) c= s + n } is set
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)
{ (b1 + s2) where b1 is Element of the carrier of t : b1 in B } is set
(t,s1,(t,s2,B)) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in (t,s2,B) } is set
(t,s1,n) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in n } is set
b2 is Element of the carrier of t
(t,b2,B) is Element of K32( the carrier of t)
{ (b1 + b2) where b1 is Element of the carrier of t : b1 in B } is set
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)
{ (b1 + (s2 + s1)) where b1 is Element of the carrier of t : b1 in B } is set
n + s is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in n & b2 in s ) } is set
(t,(n + s),B) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,B) c= n + s } is set

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)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in n ) } is set
B is Element of K32( the carrier of t)
n + B is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in n & b2 in B ) } is set
s + (n + B) is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in n + B ) } is set
(s + n) + B is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s + n & b2 in B ) } is set
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

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)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in s \/ n } is set
(t,B,s) is Element of K32( the carrier of t)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in s } is set
(t,B,n) is Element of K32( the carrier of t)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in n } is set
(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
{ (b1 + B) where b1 is Element of the carrier of t : b1 in s } is set
{ (b1 + B) where b1 is Element of the carrier of t : b1 in n } is set
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

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)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in s /\ n } is set
(t,B,s) is Element of K32( the carrier of t)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in s } is set
(t,B,n) is Element of K32( the carrier of t)
{ (b1 + B) where b1 is Element of the carrier of t : b1 in n } is set
(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
{ (b1 + B) where b1 is Element of the carrier of t : b1 in n } is set
{ (b1 + B) where b1 is Element of the carrier of t : b1 in s } is set
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

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)
{ b1 where b1 is Element of the carrier of t : (t,b1,n) c= s } is set
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)
{ b1 where b1 is Element of the carrier of t : (t,b1,(n \/ B)) c= s } is set
(t,s,B) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,B) c= s } is set
(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)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in n \/ B } is set
(t,s1,n) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in n } is set
(t,s1,B) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in B } is set
(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)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in n } is set
(t,s1,B) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in B } is set
(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)
{ (b1 + s2) where b1 is Element of the carrier of t : b1 in B } is set
(t,s1,(n \/ B)) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in n \/ B } is set

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)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in n ) } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in n \/ B ) } is set
s + B is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in B ) } is set
(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
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in n ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in B ) } is set
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

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)
{ b1 where b1 is Element of the carrier of t : (t,b1,n) c= s } is set
B is Element of K32( the carrier of t)
(t,B,n) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,n) c= B } is set
(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)
{ b1 where b1 is Element of the carrier of t : (t,b1,n) c= s \/ B } is set
x is set
s1 is Element of the carrier of t
(t,s1,n) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in n } is set
s2 is set

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)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s \/ n & b2 in B ) } is set
s + B is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in B ) } is set
n + B is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in n & b2 in B ) } is set
(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
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in B ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in n & b2 in B ) } is set
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

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)
{ b1 where b1 is Element of the carrier of t : (t,b1,B) c= s /\ n } is set
(t,s,B) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,B) c= s } is set
(t,n,B) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,B) c= n } is set
(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)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in B } is set
x is set
s1 is Element of the carrier of t
(t,s1,B) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in B } is set
s2 is set
b2 is Element of the carrier of t
(t,b2,B) is Element of K32( the carrier of t)
{ (b1 + b2) where b1 is Element of the carrier of t : b1 in B } is set

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)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s /\ n & b2 in B ) } is set
s + B is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in B ) } is set
n + B is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in n & b2 in B ) } is set
(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
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in n & b2 in B ) } is set
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in B ) } is set

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)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in n ) } is set
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)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in n /\ B ) } is set
s + B is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in B ) } is set
(s + n) /\ (s + B) is Element of K32( the carrier of t)
(n /\ B) + s is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in n /\ B & b2 in s ) } is set
n + s is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in n & b2 in s ) } is set
B + s is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in B & b2 in s ) } is set
(n + s) /\ (B + s) is Element of K32( the carrier of t)
(s + n) /\ (B + s) is Element of K32( the carrier of t)

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)
{ b1 where b1 is Element of the carrier of t : (t,b1,n) c= s } is set
B is Element of K32( the carrier of t)
(t,s,B) is Element of K32( the carrier of t)
{ b1 where b1 is Element of the carrier of t : (t,b1,B) c= s } is set
(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)
{ b1 where b1 is Element of the carrier of t : (t,b1,(n /\ B)) c= s } is set
x is set
s1 is Element of the carrier of t
(t,s1,n) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in n } is set
(t,s1,B) is Element of K32( the carrier of t)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in B } is set
(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)
{ (b1 + s1) where b1 is Element of the carrier of t : b1 in n /\ B } is set

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)
{ b1 where b1 is Element of the carrier of t : (t,b1,n) c= s ` } is set
(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)
{ (- b1) where b1 is Element of the carrier of t : b1 in n } is set
s + (t,n) is Element of K32( the carrier of t)
{ (b1 + b2) where b1, b2 is Element of the carrier of t : ( b1 in s & b2 in (t,n) ) } is set
B is set
x is Element of the carrier of t
(t,x,n) is Element of K32( the carrier of t)
{ (b1 + x) where b1 is Element of the carrier of t : b1 in n } is set
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