:: 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₁ + s) where b₁ is Element of the carrier of t : b₁ 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
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₁) where b₁ is Element of the carrier of t : b₁ in s } is set
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₁ where b₁ is Element of the carrier of t : (t,b₁,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)
{ (b₁ + x) where b₁ is Element of the carrier of t : b₁ in n } is set
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₁) where b₁ is Element of the carrier of t : b₁ in s } is set
(t,(t,s)) is Element of K32( the carrier of t)
{ (- b₁) where b₁ is Element of the carrier of t : b₁ 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
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) where b₁ is Element of the carrier of t : b₁ 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
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₁ + B) where b₁ is Element of the carrier of t : b₁ in s } is set
(t,B,n) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ 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
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₁ + s) where b₁ is Element of the carrier of t : b₁ 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
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₁ where b₁ is Element of the carrier of t : (t,b₁,{(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)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ in {(0. t)} } 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
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) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + s) where b₁ is Element of the carrier of t : b₁ 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
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₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ 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
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in {(0. t)} ) } 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 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₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in {n} ) } is set
(t,n,s) is Element of K32( the carrier of t)
{ (b₁ + n) where b₁ is Element of the carrier of t : b₁ 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
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₁ where b₁ is Element of the carrier of t : (t,b₁,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)
{ (b₁ + x) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + x) where b₁ is Element of the carrier of t : b₁ in n } 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)
B is Element of K32( the carrier of t)
(t,s,B) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,B) c= s } is set
(t,n,B) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,B) c= n } is set
s + B is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in B ) } is set
n + B is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in n & b₂ 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)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ 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
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₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= B } is set
(t,B,s) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,s) c= B } is set
B + s is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in B & b₂ in s ) } is set
B + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in B & b₂ 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)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in n } is set
(t,s1,s) is Element of K32( the carrier of t)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ 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
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₁ where b₁ is Element of the carrier of t : (t,b₁,s) c= n } is set
n + s is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in n & b₂ 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)
{ (b₁ + x) where b₁ is Element of the carrier of t : b₁ 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
{ (b₁ + x) where b₁ is Element of the carrier of t : b₁ 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
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in n & b₂ in s ) } 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₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n ) } is set
n + s is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in n & b₂ 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
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₁ + B) where b₁ is Element of the carrier of t : b₁ in s } is set
x is Element of the carrier of t
(t,x,n) is Element of K32( the carrier of t)
{ (b₁ + x) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + (B - x)) where b₁ is Element of the carrier of t : b₁ 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
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ 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
{ (b₁ + (B - x)) where b₁ is Element of the carrier of t : b₁ 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
{ (b₁ + x) where b₁ is Element of the carrier of t : b₁ in n } 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)
(t,s,n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s } is set
B is Element of the carrier of t
(t,B,s) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ in s } is set
(t,(t,B,s),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= (t,B,s) } is set
(t,B,(t,s,n)) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + (s1 - B)) where b₁ is Element of the carrier of t : b₁ 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
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + s2) where b₁ is Element of the carrier of t : b₁ in n } is set
b2 is Element of the carrier of t
(t,b2,n) is Element of K32( the carrier of t)
{ (b₁ + b2) where b₁ is Element of the carrier of t : b₁ in n } 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₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n ) } is set
B is Element of the carrier of t
(t,B,s) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ in s } is set
(t,B,s) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,B,s) & b₂ in n ) } is set
(t,B,(s + n)) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ 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
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₁ + n) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + (n + B)) where b₁ is Element of the carrier of t : b₁ 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
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₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s } is set
B is Element of the carrier of t
(t,B,n) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ in n } is set
(t,s,(t,B,n)) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,(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)
{ (b₁ + (- B)) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + (s1 + B)) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + s2) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + b2) where b₁ is Element of the carrier of t : b₁ in n } 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₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n ) } is set
B is Element of the carrier of t
(t,B,n) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ in n } is set
s + (t,B,n) is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in (t,B,n) ) } is set
(t,B,(s + n)) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ 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
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₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in n & b₂ in s ) } is set
B is Element of the carrier of t
(t,B,n) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ 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
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₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n ) } is set
(t,(s + n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,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)
{ (b₁ + x) where b₁ is Element of the carrier of t : b₁ in n } is set
n + s is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in n & b₂ in s ) } is set
(t,(n + s),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= n + s } 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
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₁ + (0. t)) where b₁ is Element of the carrier of t : b₁ 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
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₁ where b₁ is Element of the carrier of t : (t,b₁,{n}) c= s } is set
- n is Element of the carrier of t
(t,(- n),s) is Element of K32( the carrier of t)
{ (b₁ + (- n)) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + x) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + n) where b₁ is Element of the carrier of t : b₁ in {x} } is set
(t,(- n),(t,n,{x})) is Element of K32( the carrier of t)
{ (b₁ + (- n)) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + (n + (- n))) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + (0. t)) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ 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)
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₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s } is set
(t,s,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,n) & b₂ 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)
{ (b₁ + s2) where b₁ is Element of the carrier of t : b₁ in n } 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)
(t,s,n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s } is set
B is Element of K32( the carrier of t)
n + B is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in n & b₂ in B ) } is set
(t,s,(n + B)) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,(n + B)) c= s } is set
(t,(t,s,n),B) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,B) c= (t,s,n) } is set
(t,s,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,n) & b₂ 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)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in n + B } is set
(t,s1,n) is Element of K32( the carrier of t)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in n } is set
(t,s1,n) + B is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s1,n) & b₂ in B ) } is set
B + (t,s1,n) is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in B & b₂ in (t,s1,n) ) } is set
(t,(B + (t,s1,n)),(t,s1,n)) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,(t,s1,n)) c= B + (t,s1,n) } is set
(t,s,(t,s1,n)) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,(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)
{ (b₁ + (- s1)) where b₁ is Element of the carrier of t : b₁ in (t,s,n) } is set
(t,s1,B) is Element of K32( the carrier of t)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in B } is set
(t,s1,(t,(- s1),(t,s,n))) is Element of K32( the carrier of t)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + ((- s1) + s1)) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + (s1 - s1)) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + (0. t)) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in B } is set
(t,s1,B) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s1,B) & b₂ in n ) } is set
B + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in B & b₂ in n ) } is set
(t,s1,(B + n)) is Element of K32( the carrier of t)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in B + n } is set
(t,s,(B + n)) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,(B + n)) c= s } 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)
B is Element of K32( the carrier of t)
n + B is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in n & b₂ in B ) } is set
(t,s,(n + B)) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,(n + B)) c= s } is set
(t,s,B) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,B) c= s } is set
(t,(t,s,B),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= (t,s,B) } is set
B + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in B & b₂ in n ) } is set
(t,s,(B + n)) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,(B + n)) c= s } 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₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n ) } is set
B is Element of K32( the carrier of t)
(t,n,B) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,B) c= n } is set
s + (t,n,B) is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in (t,n,B) ) } is set
(t,(s + n),B) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,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)
{ (b₁ + s2) where b₁ is Element of the carrier of t : b₁ in B } is set
(t,s1,(t,s2,B)) is Element of K32( the carrier of t)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in (t,s2,B) } is set
(t,s1,n) is Element of K32( the carrier of t)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in n } is set
b2 is Element of the carrier of t
(t,b2,B) is Element of K32( the carrier of t)
{ (b₁ + b2) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + (s2 + s1)) where b₁ is Element of the carrier of t : b₁ in B } is set
n + s is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in n & b₂ in s ) } is set
(t,(n + s),B) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,B) c= n + s } 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₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n ) } is set
B is Element of K32( the carrier of t)
n + B is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in n & b₂ in B ) } is set
s + (n + B) is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n + B ) } is set
(s + n) + B is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s + n & b₂ 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
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₁ + B) where b₁ is Element of the carrier of t : b₁ in s \/ n } is set
(t,B,s) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ in s } is set
(t,B,n) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ 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
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ in s } is set
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ 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
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₁ + B) where b₁ is Element of the carrier of t : b₁ in s /\ n } is set
(t,B,s) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ in s } is set
(t,B,n) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ 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
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ in n } is set
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ 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
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₁ where b₁ is Element of the carrier of t : (t,b₁,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)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,(n \/ B)) c= s } is set
(t,s,B) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,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)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in n \/ B } is set
(t,s1,n) is Element of K32( the carrier of t)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in n } is set
(t,s1,B) is Element of K32( the carrier of t)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in n } is set
(t,s1,B) is Element of K32( the carrier of t)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + s2) where b₁ is Element of the carrier of t : b₁ in B } is set
(t,s1,(n \/ B)) is Element of K32( the carrier of t)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in n \/ B } 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₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ 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)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n \/ B ) } is set
s + B is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ 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
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n ) } is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ 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
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₁ where b₁ is Element of the carrier of t : (t,b₁,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)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,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)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,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)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in n } is set
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₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s \/ n & b₂ in B ) } is set
s + B is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in B ) } is set
n + B is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in n & b₂ 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
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in B ) } is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in n & b₂ 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
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₁ where b₁ is Element of the carrier of t : (t,b₁,B) c= s /\ n } is set
(t,s,B) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,B) c= s } is set
(t,n,B) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,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)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + b2) where b₁ is Element of the carrier of t : b₁ in B } 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₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s /\ n & b₂ in B ) } is set
s + B is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in B ) } is set
n + B is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in n & b₂ 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
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in n & b₂ in B ) } is set
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in B ) } 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₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ 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)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n /\ B ) } is set
s + B is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ 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)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in n /\ B & b₂ in s ) } is set
n + s is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in n & b₂ in s ) } is set
B + s is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in B & b₂ 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)
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₁ where b₁ is Element of the carrier of t : (t,b₁,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)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,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)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,(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)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in n } is set
(t,s1,B) is Element of K32( the carrier of t)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in n /\ B } 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)
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₁ where b₁ is Element of the carrier of t : (t,b₁,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)
{ (- b₁) where b₁ is Element of the carrier of t : b₁ in n } is set
s + (t,n) is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ 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)
{ (b₁ + x) where b₁ is Element of the carrier of t : b₁ 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 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
b2 is Element of the carrier of t
- b2 is Element of the carrier of t
x - b2 is Element of the carrier of t
x + (- b2) is Element of the carrier of t
K164( the carrier of t, the addF of t,x,(- b2)) is Element of the carrier of t
s2 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 + 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
{ (b₁ + s2) where b₁ is Element of the carrier of t : b₁ in n } is set
(t,s2,n) is Element of K32( the carrier of t)
{ (b₁ + s2) where b₁ is Element of the carrier of t : b₁ in n } is set
b1 is Element of the carrier of t
(t,b1,n) is Element of K32( the carrier of t)
{ (b₁ + b1) where b₁ is Element of the carrier of t : b₁ in n } 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)
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<sub>1</sub> where b<sub>1</sub> is Element of the carrier of t : (t,b<sub>1</sub>,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)
{ (- b₁) where b₁ is Element of the carrier of t : b₁ in n } is set
(s `) + (t,n) is Element of K32( the carrier of t)
{ (b<sub>1</sub> + b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of t : ( b<sub>1</sub> in s ` & b₂ 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)
{ (b₁ + x) where b₁ is Element of the carrier of t : b₁ 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 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
b2 is Element of the carrier of t
- b2 is Element of the carrier of t
s2 is Element of the carrier of t
x - b2 is Element of the carrier of t
x + (- b2) is Element of the carrier of t
K164( the carrier of t, the addF of t,x,(- 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 + 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
{ (b₁ + s2) where b₁ is Element of the carrier of t : b₁ in n } is set
(t,s2,n) is Element of K32( the carrier of t)
{ (b₁ + s2) where b₁ is Element of the carrier of t : b₁ in n } is set
b1 is Element of the carrier of t
(t,b1,n) is Element of K32( the carrier of t)
{ (b₁ + b1) where b₁ is Element of the carrier of t : b₁ in n } is set
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)
n is Element of K32( the carrier of t)
(t,s,n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s } is set
(t,s,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,n) & b₂ in n ) } is set
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)
n is Element of K32( the carrier of t)
s + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n ) } is set
(t,(s + n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s + n } 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)
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,n) is Element of K32( the carrier of t)
{ (- b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of t : b<sub>1</sub> in n } is set
(t,(s `),(t,n)) is Element of K32( the carrier of t)
(t,(s `),(t,n)) is Element of K32( the carrier of t)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of t : (t,b<sub>1</sub>,(t,n)) c= s ` } is set
(t,(s `),(t,n)) + (t,n) is Element of K32( the carrier of t)
{ (b<sub>1</sub> + b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of t : ( b<sub>1</sub> in (t,(s `),(t,n)) & b₂ in (t,n) ) } is set
(t,(s `),(t,n)) ` is Element of K32( the carrier of t)
the carrier of t \ (t,(s `),(t,n)) is set
(t,s,n) is Element of K32( the carrier of t)
s + n is Element of K32( the carrier of t)
{ (b<sub>1</sub> + b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of t : ( b<sub>1</sub> in s & b<sub>2</sub> in n ) } is set
(t,(s + n),n) is Element of K32( the carrier of t)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of t : (t,b<sub>1</sub>,n) c= s + n } is set
(t,(s `),(t,n)) ` is Element of K32( the carrier of t)
the carrier of t \ (t,(s `),(t,n)) is set
(t,((t,(s `),(t,n)) `),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= (t,(s `),(t,n)) ` } is set
(t,((t,(s `),(t,n)) `),n) ` is Element of K32( the carrier of t)
the carrier of t \ (t,((t,(s `),(t,n)) `),n) is set
((t,((t,(s `),(t,n)) `),n) `) ` is Element of K32( the carrier of t)
the carrier of t \ ((t,((t,(s `),(t,n)) `),n) `) is set
(t,(t,n)) is Element of K32( the carrier of t)
{ (- b₁) where b₁ is Element of the carrier of t : b₁ in (t,n) } is set
s + (t,(t,n)) is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in (t,(t,n)) ) } is set
(t,(s + (t,(t,n))),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s + (t,(t,n)) } 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)
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,n) is Element of K32( the carrier of t)
{ (- b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of t : b<sub>1</sub> in n } is set
(t,(s `),(t,n)) is Element of K32( the carrier of t)
(s `) + (t,n) is Element of K32( the carrier of t)
{ (b<sub>1</sub> + b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of t : ( b<sub>1</sub> in s ` & b₂ in (t,n) ) } is set
(t,((s `) + (t,n)),(t,n)) is Element of K32( the carrier of t)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of t : (t,b<sub>1</sub>,(t,n)) c= (s `) + (t,n) } is set
(t,(s `),(t,n)) ` is Element of K32( the carrier of t)
the carrier of t \ (t,(s `),(t,n)) is set
(t,s,n) is Element of K32( the carrier of t)
(t,s,n) is Element of K32( the carrier of t)
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of t : (t,b<sub>1</sub>,n) c= s } is set
(t,s,n) + n is Element of K32( the carrier of t)
{ (b<sub>1</sub> + b<sub>2</sub>) where b<sub>1</sub>, b<sub>2</sub> is Element of the carrier of t : ( b<sub>1</sub> in (t,s,n) & b<sub>2</sub> in n ) } is set
((s `) + (t,n)) ` is Element of K32( the carrier of t)
the carrier of t \ ((s `) + (t,n)) is set
(t,(t,n)) is Element of K32( the carrier of t)
{ (- b₁) where b₁ is Element of the carrier of t : b₁ in (t,n) } is set
(((s `) + (t,n)) `) + (t,(t,n)) is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in ((s `) + (t,n)) ` & b₂ in (t,(t,n)) ) } is set
(((s `) + (t,n)) `) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in ((s `) + (t,n)) ` & b₂ in n ) } is set
(t,s,n) ` is Element of K32( the carrier of t)
the carrier of t \ (t,s,n) is set
((t,s,n) `) ` is Element of K32( the carrier of t)
the carrier of t \ ((t,s,n) `) is set
(((t,s,n) `) `) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in ((t,s,n) `) ` & b₂ in n ) } 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)
(t,s,n) is Element of K32( the carrier of t)
(t,s,n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s } is set
(t,s,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,n) & b₂ in n ) } is set
(t,s,n) is Element of K32( the carrier of t)
s + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n ) } is set
(t,(s + n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s + 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)
{ (b₁ + s2) where b₁ is Element of the carrier of t : b₁ in n } 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)
(t,s,s) is Element of K32( the carrier of t)
(t,s,s) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,s) c= s } is set
(t,s,s) + s is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,s) & b₂ in s ) } is set
n is set
0. t is V49(t) Element of the carrier of t
(t,(0. t),s) is Element of K32( the carrier of t)
{ (b₁ + (0. t)) where b₁ is Element of the carrier of t : b₁ in s } 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 K32( the carrier of t)
(t,s,n) is Element of K32( the carrier of t)
(t,s,n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s } is set
(t,s,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,n) & b₂ in n ) } is set
(t,(t,s,n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= (t,s,n) } is set
(t,s,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,n) & b₂ in n ) } is set
s + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n ) } 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)
(t,s,n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s } is set
(t,s,n) is Element of K32( the carrier of t)
s + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n ) } is set
(t,(s + n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s + n } is set
(t,(t,s,n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= (t,s,n) } is set
(t,s,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,n) & b₂ in n ) } 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)
B is Element of K32( the carrier of t)
(t,s,B) is Element of K32( the carrier of t)
(t,s,B) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,B) c= s } is set
(t,s,B) + B is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,B) & b₂ in B ) } is set
(t,n,B) is Element of K32( the carrier of t)
(t,n,B) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,B) c= n } is set
(t,n,B) + B is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,n,B) & b₂ in B ) } is set
(t,s,B) is Element of K32( the carrier of t)
s + B is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in B ) } is set
(t,(s + B),B) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,B) c= s + B } is set
(t,n,B) is Element of K32( the carrier of t)
n + B is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in n & b₂ in B ) } is set
(t,(n + B),B) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,B) c= n + 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
(t,b2,B) is Element of K32( the carrier of t)
{ (b₁ + b2) where b₁ is Element of the carrier of t : b₁ 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)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in B } 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)
(t,s,n) is Element of K32( the carrier of t)
(t,s,n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s } is set
(t,s,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,n) & b₂ in n ) } is set
B is Element of the carrier of t
(t,B,s) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ in s } is set
(t,(t,B,s),n) is Element of K32( the carrier of t)
(t,(t,B,s),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= (t,B,s) } is set
(t,(t,B,s),n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,(t,B,s),n) & b₂ in n ) } is set
(t,B,(t,s,n)) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ in (t,s,n) } is set
(t,B,(t,s,n)) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ in (t,s,n) } is set
(t,B,(t,s,n)) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,B,(t,s,n)) & b₂ in n ) } 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)
(t,s,n) is Element of K32( the carrier of t)
s + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n ) } is set
(t,(s + n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s + n } is set
B is Element of the carrier of t
(t,B,s) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ in s } is set
(t,(t,B,s),n) is Element of K32( the carrier of t)
(t,B,s) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,B,s) & b₂ in n ) } is set
(t,((t,B,s) + n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= (t,B,s) + n } is set
(t,B,(t,s,n)) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ in (t,s,n) } is set
(t,B,(s + n)) is Element of K32( the carrier of t)
{ (b₁ + B) where b₁ is Element of the carrier of t : b₁ in s + n } is set
(t,(t,B,(s + n)),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= (t,B,(s + n)) } 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)
B is Element of K32( the carrier of t)
(t,B,n) is Element of K32( the carrier of t)
(t,B,n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= B } is set
(t,B,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,B,n) & b₂ in n ) } is set
(t,B,s) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,s) c= B } is set
(t,B,s) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,B,s) & b₂ in 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
(t,b2,n) is Element of K32( the carrier of t)
{ (b₁ + b2) where b₁ is Element of the carrier of t : b₁ in n } is set
(t,b2,s) is Element of K32( the carrier of t)
{ (b₁ + b2) where b₁ is Element of the carrier of t : b₁ in s } 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)
B is Element of K32( the carrier of t)
(t,B,s) is Element of K32( the carrier of t)
B + s is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in B & b₂ in s ) } is set
(t,(B + s),s) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,s) c= B + s } is set
B + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in B & b₂ in n ) } is set
(t,(B + n),s) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,s) c= B + n } is set
x is set
s1 is Element of the carrier of t
(t,s1,s) is Element of K32( the carrier of t)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in s } 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₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n ) } is set
(t,s,n) is Element of K32( the carrier of t)
(t,(s + n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s + n } is set
(t,s,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,n) & b₂ in n ) } is set
(t,s,n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s } is set
(t,s,n) is Element of K32( the carrier of t)
(t,s,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,n) & b₂ in n ) } is set
(t,(t,s,n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= (t,s,n) } is set
(t,(s + n),n) is Element of K32( the carrier of t)
(t,(s + n),n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,(s + n),n) & b₂ in n ) } is set
(t,(t,s,n),n) is Element of K32( the carrier of t)
(t,((t,s,n) + n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= (t,s,n) + n } 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₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n ) } is set
(t,(s + n),n) is Element of K32( the carrier of t)
(t,(s + n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s + n } is set
(t,(s + n),n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,(s + n),n) & b₂ in n ) } is set
(t,s,n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s } is set
(t,(t,s,n),n) is Element of K32( the carrier of t)
(t,s,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,n) & b₂ in n ) } is set
(t,((t,s,n) + n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= (t,s,n) + n } is set
(t,s,n) is Element of K32( the carrier of t)
(t,s,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,n) & b₂ in n ) } is set
(t,s,n) is Element of K32( the carrier of t)
(t,(t,s,n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= (t,s,n) } 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)
(t,s,n) is Element of K32( the carrier of t)
(t,s,n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s } is set
(t,s,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,n) & b₂ in n ) } is set
(t,(t,s,n),n) is Element of K32( the carrier of t)
(t,(t,s,n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= (t,s,n) } is set
(t,(t,s,n),n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,(t,s,n),n) & b₂ 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)
{ (b₁ + s2) where b₁ is Element of the carrier of t : b₁ in n } is set
(t,(t,s2,n),n) is Element of K32( the carrier of t)
(t,(t,s2,n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= (t,s2,n) } is set
(t,(t,s2,n),n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,(t,s2,n),n) & b₂ in n ) } is set
(t,n,n) is Element of K32( the carrier of t)
(t,n,n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= n } is set
(t,n,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,n,n) & b₂ in n ) } is set
(t,s2,(t,n,n)) is Element of K32( the carrier of t)
{ (b₁ + s2) where b₁ is Element of the carrier of t : b₁ in (t,n,n) } 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)
(t,s,n) is Element of K32( the carrier of t)
s + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in s & b₂ in n ) } is set
(t,(s + n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s + n } is set
(t,(t,s,n),n) is Element of K32( the carrier of t)
(t,s,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,n) & b₂ in n ) } is set
(t,((t,s,n) + n),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= (t,s,n) + n } 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)
(t,s,n) is Element of K32( the carrier of t)
(t,s,n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s } is set
(t,s,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,n) & b₂ in n ) } is set
B 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)
(t,(s \/ B),n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s \/ B } is set
(t,(s \/ B),n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,(s \/ B),n) & b₂ in n ) } 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)
(t,s,n) is Element of K32( the carrier of t)
(t,s,n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s } is set
(t,s,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,s,n) & b₂ in n ) } is set
B is Element of K32( the carrier of t)
(t,B,s) is Element of K32( the carrier of t)
(t,B,s) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,s) c= B } is set
(t,B,s) + s is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,B,s) & b₂ in s ) } is set
(t,B,n) is Element of K32( the carrier of t)
(t,B,n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= B } is set
(t,B,n) + n is Element of K32( the carrier of t)
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of t : ( b₁ in (t,B,n) & b₂ in 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
(t,b2,s) is Element of K32( the carrier of t)
{ (b₁ + b2) where b₁ is Element of the carrier of t : b₁ in s } is set
b1 is Element of the carrier of t
b1 is Element of the carrier of t
b1 + b1 is Element of the carrier of t
K164( the carrier of t, the addF of t,b1,b1) is Element of the carrier of t
x4 is Element of the carrier of t
(t,x4,n) is Element of K32( the carrier of t)
{ (b₁ + x4) where b₁ is Element of the carrier of t : b₁ in n } is set
(t,b2,(t,x4,n)) is Element of K32( the carrier of t)
{ (b₁ + b2) where b₁ is Element of the carrier of t : b₁ in (t,x4,n) } is set
(t,b1,n) is Element of K32( the carrier of t)
{ (b₁ + b1) where b₁ is Element of the carrier of t : b₁ in n } is set
(t,s1,(t,b1,n)) is Element of K32( the carrier of t)
{ (b₁ + s1) where b₁ is Element of the carrier of t : b₁ in (t,b1,n) } is set
b1 + s1 is Element of the carrier of t
K164( the carrier of t, the addF of t,b1,s1) is Element of the carrier of t
(t,(b1 + s1),n) is Element of K32( the carrier of t)
{ (b₁ + (b1 + s1)) where b₁ is Element of the carrier of t : b₁ in n } is set
s1 + b1 is Element of the carrier of t
K164( the carrier of t, the addF of t,s1,b1) is Element of the carrier of t
(s1 + b1) + b1 is Element of the carrier of t
K164( the carrier of t, the addF of t,(s1 + b1),b1) is Element of the carrier of t
s is non empty RLSStruct
the carrier of s is non empty set
K32( the carrier of s) is set
t is V24() real ext-real set
n is Element of K32( the carrier of s)
{ (t * b₁) where b₁ is Element of the carrier of s : b₁ in n } is set
B is set
x is Element of the carrier of s
t * x is Element of the carrier of s
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)
(0,t,s) is Element of K32( the carrier of t)
{ (0 * b₁) where b₁ is Element of the carrier of t : b₁ in s } is set
n is set
B is Element of the carrier of t
0 * B is Element of the carrier of t
t is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL t 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 t) is non empty set
K32( the carrier of (TOP-REAL t)) is set
0. (TOP-REAL t) is V40(t) V49( TOP-REAL t) V83() V126() Element of the carrier of (TOP-REAL t)
{(0. (TOP-REAL t))} is non empty Element of K32( the carrier of (TOP-REAL t))
n is non empty Element of K32( the carrier of (TOP-REAL t))
(0,(TOP-REAL t),n) is Element of K32( the carrier of (TOP-REAL t))
{ (0 * b₁) where b₁ is Element of the carrier of (TOP-REAL t) : b₁ in n } is set
B is set
x is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
0 * x is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
B is set
the Element of n is Element of n
{B} is non empty set
s1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
0 * s1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
t is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL t 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 t) is non empty set
K32( the carrier of (TOP-REAL t)) is set
s is Element of K32( the carrier of (TOP-REAL t))
(1,(TOP-REAL t),s) is Element of K32( the carrier of (TOP-REAL t))
{ (1 * b₁) where b₁ is Element of the carrier of (TOP-REAL t) : b₁ in s } is set
n is set
B is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
1 * B is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
n is set
B is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
1 * B is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
t is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL t 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 t) is non empty set
K32( the carrier of (TOP-REAL t)) is set
s is Element of K32( the carrier of (TOP-REAL t))
(2,(TOP-REAL t),s) is Element of K32( the carrier of (TOP-REAL t))
{ (2 * b₁) where b₁ is Element of the carrier of (TOP-REAL t) : b₁ in s } is set
s + s is Element of K32( the carrier of (TOP-REAL t))
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of (TOP-REAL t) : ( b₁ in s & b₂ in s ) } is set
n is set
B is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
2 * B is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
1 + 1 is non empty V24() real ext-real positive non negative Element of REAL
(1 + 1) * B is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
1 * B is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(1 * B) + (1 * B) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
the addF of (TOP-REAL t) is V12() V30(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)) Element of K32(K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)))
K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)) is set
K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)) is set
K32(K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t))) is set
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(1 * B),(1 * B)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
B + (1 * B) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),B,(1 * B)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
B + B is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),B,B) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
t is V24() real ext-real set
s is V24() real ext-real set
t * s is V24() real ext-real set
n is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL n 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 n) is non empty set
K32( the carrier of (TOP-REAL n)) is set
B is Element of K32( the carrier of (TOP-REAL n))
((t * s),(TOP-REAL n),B) is Element of K32( the carrier of (TOP-REAL n))
{ ((t * s) * b₁) where b₁ is Element of the carrier of (TOP-REAL n) : b₁ in B } is set
(s,(TOP-REAL n),B) is Element of K32( the carrier of (TOP-REAL n))
{ (s * b₁) where b₁ is Element of the carrier of (TOP-REAL n) : b₁ in B } is set
(t,(TOP-REAL n),(s,(TOP-REAL n),B)) is Element of K32( the carrier of (TOP-REAL n))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL n) : b₁ in (s,(TOP-REAL n),B) } is set
x is set
s1 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
(t * s) * s1 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
s * s1 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
t * (s * s1) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
x is set
s1 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
t * s1 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
s2 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
s * s2 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
(t * s) * s2 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
t is V24() real ext-real set
s is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL s 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 s) is non empty set
K32( the carrier of (TOP-REAL s)) is set
n is Element of K32( the carrier of (TOP-REAL s))
(t,(TOP-REAL s),n) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in n } is set
B is Element of K32( the carrier of (TOP-REAL s))
(t,(TOP-REAL s),B) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in B } is set
x is set
s1 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
t * s1 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
t is V24() real ext-real set
s is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL s 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 s) is non empty set
K32( the carrier of (TOP-REAL s)) is set
n is Element of K32( the carrier of (TOP-REAL s))
(t,(TOP-REAL s),n) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in n } is set
B is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
((TOP-REAL s),B,n) is Element of K32( the carrier of (TOP-REAL s))
{ (b₁ + B) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in n } is set
(t,(TOP-REAL s),((TOP-REAL s),B,n)) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in ((TOP-REAL s),B,n) } is set
t * B is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
((TOP-REAL s),(t * B),(t,(TOP-REAL s),n)) is Element of K32( the carrier of (TOP-REAL s))
{ (b₁ + (t * B)) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in (t,(TOP-REAL s),n) } is set
x is set
s1 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
t * s1 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
s2 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
s2 + B is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
the addF of (TOP-REAL s) is V12() V30(K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)), the carrier of (TOP-REAL s)) Element of K32(K33(K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)), the carrier of (TOP-REAL s)))
K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)) is set
K33(K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)), the carrier of (TOP-REAL s)) is set
K32(K33(K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)), the carrier of (TOP-REAL s))) is set
K164( the carrier of (TOP-REAL s), the addF of (TOP-REAL s),s2,B) is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
t * s2 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
(t * s2) + (t * B) is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
K164( the carrier of (TOP-REAL s), the addF of (TOP-REAL s),(t * s2),(t * B)) is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
x is set
s1 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
s1 + (t * B) is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
the addF of (TOP-REAL s) is V12() V30(K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)), the carrier of (TOP-REAL s)) Element of K32(K33(K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)), the carrier of (TOP-REAL s)))
K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)) is set
K33(K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)), the carrier of (TOP-REAL s)) is set
K32(K33(K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)), the carrier of (TOP-REAL s))) is set
K164( the carrier of (TOP-REAL s), the addF of (TOP-REAL s),s1,(t * B)) is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
s2 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
t * s2 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
s2 + B is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
K164( the carrier of (TOP-REAL s), the addF of (TOP-REAL s),s2,B) is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
t * (s2 + B) is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
t is V24() real ext-real set
s is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL s 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 s) is non empty set
K32( the carrier of (TOP-REAL s)) is set
n is Element of K32( the carrier of (TOP-REAL s))
(t,(TOP-REAL s),n) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in n } is set
B is Element of K32( the carrier of (TOP-REAL s))
n + B is Element of K32( the carrier of (TOP-REAL s))
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of (TOP-REAL s) : ( b₁ in n & b₂ in B ) } is set
(t,(TOP-REAL s),(n + B)) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in n + B } is set
(t,(TOP-REAL s),B) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in B } is set
(t,(TOP-REAL s),n) + (t,(TOP-REAL s),B) is Element of K32( the carrier of (TOP-REAL s))
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of (TOP-REAL s) : ( b₁ in (t,(TOP-REAL s),n) & b₂ in (t,(TOP-REAL s),B) ) } is set
x is set
s1 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
t * s1 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
s2 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
b2 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
s2 + b2 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
the addF of (TOP-REAL s) is V12() V30(K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)), the carrier of (TOP-REAL s)) Element of K32(K33(K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)), the carrier of (TOP-REAL s)))
K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)) is set
K33(K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)), the carrier of (TOP-REAL s)) is set
K32(K33(K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)), the carrier of (TOP-REAL s))) is set
K164( the carrier of (TOP-REAL s), the addF of (TOP-REAL s),s2,b2) is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
t * s2 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
t * b2 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
(t * s2) + (t * b2) is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
K164( the carrier of (TOP-REAL s), the addF of (TOP-REAL s),(t * s2),(t * b2)) is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
x is set
s1 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
s2 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
s1 + s2 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
the addF of (TOP-REAL s) is V12() V30(K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)), the carrier of (TOP-REAL s)) Element of K32(K33(K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)), the carrier of (TOP-REAL s)))
K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)) is set
K33(K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)), the carrier of (TOP-REAL s)) is set
K32(K33(K33( the carrier of (TOP-REAL s), the carrier of (TOP-REAL s)), the carrier of (TOP-REAL s))) is set
K164( the carrier of (TOP-REAL s), the addF of (TOP-REAL s),s1,s2) is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
b2 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
t * b2 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
b1 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
t * b1 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
b1 + b2 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
K164( the carrier of (TOP-REAL s), the addF of (TOP-REAL s),b1,b2) is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
t * (b1 + b2) is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
t is V24() real ext-real set
s is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL s 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 s) is non empty set
K32( the carrier of (TOP-REAL s)) is set
n is Element of K32( the carrier of (TOP-REAL s))
(t,(TOP-REAL s),n) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in n } is set
B is Element of K32( the carrier of (TOP-REAL s))
((TOP-REAL s),n,B) is Element of K32( the carrier of (TOP-REAL s))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL s) : ((TOP-REAL s),b₁,B) c= n } is set
(t,(TOP-REAL s),((TOP-REAL s),n,B)) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in ((TOP-REAL s),n,B) } is set
(t,(TOP-REAL s),B) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in B } is set
((TOP-REAL s),(t,(TOP-REAL s),n),(t,(TOP-REAL s),B)) is Element of K32( the carrier of (TOP-REAL s))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL s) : ((TOP-REAL s),b₁,(t,(TOP-REAL s),B)) c= (t,(TOP-REAL s),n) } is set
x is set
s1 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
t * s1 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
s2 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
((TOP-REAL s),s2,B) is Element of K32( the carrier of (TOP-REAL s))
{ (b₁ + s2) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in B } is set
(t,(TOP-REAL s),((TOP-REAL s),s2,B)) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in ((TOP-REAL s),s2,B) } is set
t * s2 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
((TOP-REAL s),(t * s2),(t,(TOP-REAL s),B)) is Element of K32( the carrier of (TOP-REAL s))
{ (b₁ + (t * s2)) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in (t,(TOP-REAL s),B) } is set
x is set
s1 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
((TOP-REAL s),s1,(t,(TOP-REAL s),B)) is Element of K32( the carrier of (TOP-REAL s))
{ (b₁ + s1) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in (t,(TOP-REAL s),B) } is set
1 / t is V24() real ext-real Element of REAL
((1 / t),(TOP-REAL s),((TOP-REAL s),s1,(t,(TOP-REAL s),B))) is Element of K32( the carrier of (TOP-REAL s))
{ ((1 / t) * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in ((TOP-REAL s),s1,(t,(TOP-REAL s),B)) } is set
((1 / t),(TOP-REAL s),(t,(TOP-REAL s),n)) is Element of K32( the carrier of (TOP-REAL s))
{ ((1 / t) * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in (t,(TOP-REAL s),n) } is set
(1 / t) * t is V24() real ext-real Element of REAL
(((1 / t) * t),(TOP-REAL s),n) is Element of K32( the carrier of (TOP-REAL s))
{ (((1 / t) * t) * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in n } is set
(1 / t) * s1 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
((1 / t),(TOP-REAL s),(t,(TOP-REAL s),B)) is Element of K32( the carrier of (TOP-REAL s))
{ ((1 / t) * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in (t,(TOP-REAL s),B) } is set
((TOP-REAL s),((1 / t) * s1),((1 / t),(TOP-REAL s),(t,(TOP-REAL s),B))) is Element of K32( the carrier of (TOP-REAL s))
{ (b₁ + ((1 / t) * s1)) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in ((1 / t),(TOP-REAL s),(t,(TOP-REAL s),B)) } is set
(((1 / t) * t),(TOP-REAL s),B) is Element of K32( the carrier of (TOP-REAL s))
{ (((1 / t) * t) * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in B } is set
((TOP-REAL s),((1 / t) * s1),(((1 / t) * t),(TOP-REAL s),B)) is Element of K32( the carrier of (TOP-REAL s))
{ (b₁ + ((1 / t) * s1)) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in (((1 / t) * t),(TOP-REAL s),B) } is set
(1,(TOP-REAL s),B) is Element of K32( the carrier of (TOP-REAL s))
{ (1 * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in B } is set
((TOP-REAL s),((1 / t) * s1),(1,(TOP-REAL s),B)) is Element of K32( the carrier of (TOP-REAL s))
{ (b₁ + ((1 / t) * s1)) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in (1,(TOP-REAL s),B) } is set
(1,(TOP-REAL s),n) is Element of K32( the carrier of (TOP-REAL s))
{ (1 * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in n } is set
((TOP-REAL s),((1 / t) * s1),B) is Element of K32( the carrier of (TOP-REAL s))
{ (b₁ + ((1 / t) * s1)) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in B } is set
t * ((1 / t) * s1) is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
((1 / t) * t) * s1 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
1 * s1 is V40(s) V83() V126() Element of the carrier of (TOP-REAL s)
t is V24() real ext-real set
s is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL s 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 s) is non empty set
K32( the carrier of (TOP-REAL s)) is set
n is Element of K32( the carrier of (TOP-REAL s))
(t,(TOP-REAL s),n) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in n } is set
B is Element of K32( the carrier of (TOP-REAL s))
((TOP-REAL s),n,B) is Element of K32( the carrier of (TOP-REAL s))
((TOP-REAL s),n,B) is Element of K32( the carrier of (TOP-REAL s))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL s) : ((TOP-REAL s),b₁,B) c= n } is set
((TOP-REAL s),n,B) + B is Element of K32( the carrier of (TOP-REAL s))
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of (TOP-REAL s) : ( b₁ in ((TOP-REAL s),n,B) & b₂ in B ) } is set
(t,(TOP-REAL s),((TOP-REAL s),n,B)) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in ((TOP-REAL s),n,B) } is set
(t,(TOP-REAL s),B) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in B } is set
((TOP-REAL s),(t,(TOP-REAL s),n),(t,(TOP-REAL s),B)) is Element of K32( the carrier of (TOP-REAL s))
((TOP-REAL s),(t,(TOP-REAL s),n),(t,(TOP-REAL s),B)) is Element of K32( the carrier of (TOP-REAL s))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL s) : ((TOP-REAL s),b₁,(t,(TOP-REAL s),B)) c= (t,(TOP-REAL s),n) } is set
((TOP-REAL s),(t,(TOP-REAL s),n),(t,(TOP-REAL s),B)) + (t,(TOP-REAL s),B) is Element of K32( the carrier of (TOP-REAL s))
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of (TOP-REAL s) : ( b₁ in ((TOP-REAL s),(t,(TOP-REAL s),n),(t,(TOP-REAL s),B)) & b₂ in (t,(TOP-REAL s),B) ) } is set
(t,(TOP-REAL s),((TOP-REAL s),n,B)) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in ((TOP-REAL s),n,B) } is set
(t,(TOP-REAL s),((TOP-REAL s),n,B)) + (t,(TOP-REAL s),B) is Element of K32( the carrier of (TOP-REAL s))
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of (TOP-REAL s) : ( b₁ in (t,(TOP-REAL s),((TOP-REAL s),n,B)) & b₂ in (t,(TOP-REAL s),B) ) } is set
t is V24() real ext-real set
s is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL s 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 s) is non empty set
K32( the carrier of (TOP-REAL s)) is set
n is Element of K32( the carrier of (TOP-REAL s))
(t,(TOP-REAL s),n) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in n } is set
B is Element of K32( the carrier of (TOP-REAL s))
((TOP-REAL s),n,B) is Element of K32( the carrier of (TOP-REAL s))
n + B is Element of K32( the carrier of (TOP-REAL s))
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of (TOP-REAL s) : ( b₁ in n & b₂ in B ) } is set
((TOP-REAL s),(n + B),B) is Element of K32( the carrier of (TOP-REAL s))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL s) : ((TOP-REAL s),b₁,B) c= n + B } is set
(t,(TOP-REAL s),((TOP-REAL s),n,B)) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in ((TOP-REAL s),n,B) } is set
(t,(TOP-REAL s),B) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in B } is set
((TOP-REAL s),(t,(TOP-REAL s),n),(t,(TOP-REAL s),B)) is Element of K32( the carrier of (TOP-REAL s))
(t,(TOP-REAL s),n) + (t,(TOP-REAL s),B) is Element of K32( the carrier of (TOP-REAL s))
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of (TOP-REAL s) : ( b₁ in (t,(TOP-REAL s),n) & b₂ in (t,(TOP-REAL s),B) ) } is set
((TOP-REAL s),((t,(TOP-REAL s),n) + (t,(TOP-REAL s),B)),(t,(TOP-REAL s),B)) is Element of K32( the carrier of (TOP-REAL s))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL s) : ((TOP-REAL s),b₁,(t,(TOP-REAL s),B)) c= (t,(TOP-REAL s),n) + (t,(TOP-REAL s),B) } is set
(t,(TOP-REAL s),(n + B)) is Element of K32( the carrier of (TOP-REAL s))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL s) : b₁ in n + B } is set
((TOP-REAL s),(t,(TOP-REAL s),(n + B)),(t,(TOP-REAL s),B)) is Element of K32( the carrier of (TOP-REAL s))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL s) : ((TOP-REAL s),b₁,(t,(TOP-REAL s),B)) c= (t,(TOP-REAL s),(n + B)) } is set
t is non empty 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₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s } is set
s ` is Element of K32( the carrier of t)
the carrier of t \ s is set
B is Element of K32( the carrier of t)
(t,(s `),B) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,B) c= s ` } is set
(t,s,n) /\ (t,(s `),B) is Element of K32( the carrier of t)
t is non empty 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,n,B) is Element of K32( the carrier of t)
(t,s,n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s } is set
s ` is Element of K32( the carrier of t)
the carrier of t \ s is set
(t,(s `),B) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,B) c= s ` } is set
(t,s,n) /\ (t,(s `),B) is Element of K32( the carrier of t)
s \/ (t,s,n,B) is Element of K32( the carrier of t)
t is non empty 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,n,B) is Element of K32( the carrier of t)
(t,s,n) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,n) c= s } is set
s ` is Element of K32( the carrier of t)
the carrier of t \ s is set
(t,(s `),B) is Element of K32( the carrier of t)
{ b₁ where b₁ is Element of the carrier of t : (t,b₁,B) c= s ` } is set
(t,s,n) /\ (t,(s `),B) is Element of K32( the carrier of t)
s \ (t,s,n,B) is Element of K32( the carrier of t)
t is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL t 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 t) is non empty set
K32( the carrier of (TOP-REAL t)) is set
s is Element of K32( the carrier of (TOP-REAL t))
n is Element of K32( the carrier of (TOP-REAL t))
n ` is Element of K32( the carrier of (TOP-REAL t))
the carrier of (TOP-REAL t) \ n is set
B is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),n,s,B) is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),n,s) is Element of K32( the carrier of (TOP-REAL t))
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b<sub>1</sub>,s) c= n } is set
((TOP-REAL t),(n `),B) is Element of K32( the carrier of (TOP-REAL t))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b₁,B) c= n ` } is set
((TOP-REAL t),n,s) /\ ((TOP-REAL t),(n `),B) is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),(n `),B) /\ the carrier of (TOP-REAL t) is Element of K32( the carrier of (TOP-REAL t))
t is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL t 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 t) is non empty set
K32( the carrier of (TOP-REAL t)) is set
s is Element of K32( the carrier of (TOP-REAL t))
n is Element of K32( the carrier of (TOP-REAL t))
B is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),n,B,s) is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),n,B) is Element of K32( the carrier of (TOP-REAL t))
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b<sub>1</sub>,B) c= n } is set
n ` is Element of K32( the carrier of (TOP-REAL t))
the carrier of (TOP-REAL t) \ n is set
((TOP-REAL t),(n `),s) is Element of K32( the carrier of (TOP-REAL t))
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b<sub>1</sub>,s) c= n ` } is set
((TOP-REAL t),n,B) /\ ((TOP-REAL t),(n `),s) is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),n,B) /\ the carrier of (TOP-REAL t) is Element of K32( the carrier of (TOP-REAL t))
t is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL t 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 t) is non empty set
K32( the carrier of (TOP-REAL t)) is set
0. (TOP-REAL t) is V40(t) V49( TOP-REAL t) V83() V126() Element of the carrier of (TOP-REAL t)
s is Element of K32( the carrier of (TOP-REAL t))
n is Element of K32( the carrier of (TOP-REAL t))
B is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),n,s,B) is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),n,s) is Element of K32( the carrier of (TOP-REAL t))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b₁,s) c= n } is set
n ` is Element of K32( the carrier of (TOP-REAL t))
the carrier of (TOP-REAL t) \ n is set
((TOP-REAL t),(n `),B) is Element of K32( the carrier of (TOP-REAL t))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b₁,B) c= n ` } is set
((TOP-REAL t),n,s) /\ ((TOP-REAL t),(n `),B) is Element of K32( the carrier of (TOP-REAL t))
x is set
s1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((TOP-REAL t),s1,s) is Element of K32( the carrier of (TOP-REAL t))
{ (b₁ + s1) where b₁ is Element of the carrier of (TOP-REAL t) : b₁ in s } is set
(0. (TOP-REAL t)) + s1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
the addF of (TOP-REAL t) is V12() V30(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)) Element of K32(K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)))
K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)) is set
K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)) is set
K32(K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t))) is set
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(0. (TOP-REAL t)),s1) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
{ (b₁ + s1) where b₁ is V40(t) V83() V126() Element of the carrier of (TOP-REAL t) : b₁ in s } is set
t is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL t 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 t) is non empty set
K32( the carrier of (TOP-REAL t)) is set
0. (TOP-REAL t) is V40(t) V49( TOP-REAL t) V83() V126() Element of the carrier of (TOP-REAL t)
s is Element of K32( the carrier of (TOP-REAL t))
n is Element of K32( the carrier of (TOP-REAL t))
B is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),n,B,s) is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),n,B) is Element of K32( the carrier of (TOP-REAL t))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b₁,B) c= n } is set
n ` is Element of K32( the carrier of (TOP-REAL t))
the carrier of (TOP-REAL t) \ n is set
((TOP-REAL t),(n `),s) is Element of K32( the carrier of (TOP-REAL t))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b₁,s) c= n ` } is set
((TOP-REAL t),n,B) /\ ((TOP-REAL t),(n `),s) is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),n,B,s) /\ n is Element of K32( the carrier of (TOP-REAL t))
x is set
s1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((TOP-REAL t),s1,s) is Element of K32( the carrier of (TOP-REAL t))
{ (b₁ + s1) where b₁ is Element of the carrier of (TOP-REAL t) : b₁ in s } is set
(0. (TOP-REAL t)) + s1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
the addF of (TOP-REAL t) is V12() V30(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)) Element of K32(K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)))
K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)) is set
K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)) is set
K32(K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t))) is set
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(0. (TOP-REAL t)),s1) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
{ (b₁ + s1) where b₁ is V40(t) V83() V126() Element of the carrier of (TOP-REAL t) : b₁ in s } is set
t is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL t 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 t) is non empty set
K32( the carrier of (TOP-REAL t)) is set
0. (TOP-REAL t) is V40(t) V49( TOP-REAL t) V83() V126() Element of the carrier of (TOP-REAL t)
s is Element of K32( the carrier of (TOP-REAL t))
n is Element of K32( the carrier of (TOP-REAL t))
B is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),n,s,B) is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),n,s,B) is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),n,s) is Element of K32( the carrier of (TOP-REAL t))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b₁,s) c= n } is set
n ` is Element of K32( the carrier of (TOP-REAL t))
the carrier of (TOP-REAL t) \ n is set
((TOP-REAL t),(n `),B) is Element of K32( the carrier of (TOP-REAL t))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b₁,B) c= n ` } is set
((TOP-REAL t),n,s) /\ ((TOP-REAL t),(n `),B) is Element of K32( the carrier of (TOP-REAL t))
n \/ ((TOP-REAL t),n,s,B) is Element of K32( the carrier of (TOP-REAL t))
x is set
s1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((TOP-REAL t),s1,s) is Element of K32( the carrier of (TOP-REAL t))
{ (b₁ + s1) where b₁ is Element of the carrier of (TOP-REAL t) : b₁ in s } is set
(0. (TOP-REAL t)) + s1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
the addF of (TOP-REAL t) is V12() V30(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)) Element of K32(K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)))
K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)) is set
K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)) is set
K32(K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t))) is set
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(0. (TOP-REAL t)),s1) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
{ (b₁ + s1) where b₁ is V40(t) V83() V126() Element of the carrier of (TOP-REAL t) : b₁ in s } is set
t is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL t 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 t) is non empty set
K32( the carrier of (TOP-REAL t)) is set
0. (TOP-REAL t) is V40(t) V49( TOP-REAL t) V83() V126() Element of the carrier of (TOP-REAL t)
s is Element of K32( the carrier of (TOP-REAL t))
n is Element of K32( the carrier of (TOP-REAL t))
B is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),n,B,s) is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),n,B,s) is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),n,B) is Element of K32( the carrier of (TOP-REAL t))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b₁,B) c= n } is set
n ` is Element of K32( the carrier of (TOP-REAL t))
the carrier of (TOP-REAL t) \ n is set
((TOP-REAL t),(n `),s) is Element of K32( the carrier of (TOP-REAL t))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b₁,s) c= n ` } is set
((TOP-REAL t),n,B) /\ ((TOP-REAL t),(n `),s) is Element of K32( the carrier of (TOP-REAL t))
n \ ((TOP-REAL t),n,B,s) is Element of K32( the carrier of (TOP-REAL t))
x is set
x is set
s1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((TOP-REAL t),s1,s) is Element of K32( the carrier of (TOP-REAL t))
{ (b₁ + s1) where b₁ is Element of the carrier of (TOP-REAL t) : b₁ in s } is set
(0. (TOP-REAL t)) + s1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
the addF of (TOP-REAL t) is V12() V30(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)) Element of K32(K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)))
K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)) is set
K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)) is set
K32(K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t))) is set
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(0. (TOP-REAL t)),s1) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
{ (b₁ + s1) where b₁ is V40(t) V83() V126() Element of the carrier of (TOP-REAL t) : b₁ in s } is set
t is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL t 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 t) is non empty set
K32( the carrier of (TOP-REAL t)) is set
s is Element of K32( the carrier of (TOP-REAL t))
s ` is Element of K32( the carrier of (TOP-REAL t))
the carrier of (TOP-REAL t) \ s is set
n is Element of K32( the carrier of (TOP-REAL t))
B is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),s,n,B) is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),s,n,B) is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),s,n) is Element of K32( the carrier of (TOP-REAL t))
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b<sub>1</sub>,n) c= s } is set
((TOP-REAL t),(s `),B) is Element of K32( the carrier of (TOP-REAL t))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b₁,B) c= s ` } is set
((TOP-REAL t),s,n) /\ ((TOP-REAL t),(s `),B) is Element of K32( the carrier of (TOP-REAL t))
s \ ((TOP-REAL t),s,n,B) is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),(s `),B,n) is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),(s `),B,n) is Element of K32( the carrier of (TOP-REAL t))
(s `) ` is Element of K32( the carrier of (TOP-REAL t))
the carrier of (TOP-REAL t) \ (s `) is set
((TOP-REAL t),((s `) `),n) is Element of K32( the carrier of (TOP-REAL t))
{ b<sub>1</sub> where b<sub>1</sub> is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b<sub>1</sub>,n) c= (s `) ` } is set
((TOP-REAL t),(s `),B) /\ ((TOP-REAL t),((s `) `),n) is Element of K32( the carrier of (TOP-REAL t))
(s `) \/ ((TOP-REAL t),(s `),B,n) is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),(s `),B,n) ` is Element of K32( the carrier of (TOP-REAL t))
the carrier of (TOP-REAL t) \ ((TOP-REAL t),(s `),B,n) is set
s \ (((TOP-REAL t),(s `),B) /\ ((TOP-REAL t),((s `) `),n)) is Element of K32( the carrier of (TOP-REAL t))
(s \ (((TOP-REAL t),(s `),B) /\ ((TOP-REAL t),((s `) `),n))) ` is Element of K32( the carrier of (TOP-REAL t))
the carrier of (TOP-REAL t) \ (s \ (((TOP-REAL t),(s `),B) /\ ((TOP-REAL t),((s `) `),n))) is set
((s \ (((TOP-REAL t),(s `),B) /\ ((TOP-REAL t),((s `) `),n))) `) ` is Element of K32( the carrier of (TOP-REAL t))
the carrier of (TOP-REAL t) \ ((s \ (((TOP-REAL t),(s `),B) /\ ((TOP-REAL t),((s `) `),n))) `) is set
t is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital 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
B is Element of the carrier of t
x is V24() real ext-real set
x * n is Element of the carrier of t
1 - x is V24() real ext-real Element of REAL
(1 - x) * B is Element of the carrier of t
(x * n) + ((1 - x) * 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,(x * n),((1 - x) * B)) is Element of the carrier of t
((1 - x) * B) + (x * n) is Element of the carrier of t
K164( the carrier of t, the addF of t,((1 - x) * B),(x * n)) is Element of the carrier of t
{ (((1 - b₁) * B) + (b₁ * n)) where b₁ is V24() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
LSeg (n,B) is Element of K32( the carrier of t)
x is V24() real ext-real set
n is Element of the carrier of t
B is Element of the carrier of t
x * n is Element of the carrier of t
1 - x is V24() real ext-real Element of REAL
(1 - x) * B is Element of the carrier of t
(x * n) + ((1 - x) * 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,(x * n),((1 - x) * B)) is Element of the carrier of t
n is Element of the carrier of t
B is Element of the carrier of t
LSeg (n,B) is Element of K32( the carrier of t)
x is set
{ (((1 - b₁) * B) + (b₁ * n)) where b₁ is V24() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= 1 ) } is set
s1 is V24() real ext-real Element of REAL
1 - s1 is V24() real ext-real Element of REAL
(1 - s1) * B is Element of the carrier of t
s1 * n is Element of the carrier of t
((1 - s1) * B) + (s1 * 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,((1 - s1) * B),(s1 * n)) is Element of the carrier of t
x is V24() real ext-real set
n is Element of the carrier of t
B is Element of the carrier of t
x * n is Element of the carrier of t
1 - x is V24() real ext-real Element of REAL
(1 - x) * B is Element of the carrier of t
(x * n) + ((1 - x) * 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,(x * n),((1 - x) * B)) is Element of the carrier of t
t is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital 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)
x is V24() real ext-real set
n is Element of the carrier of t
B is Element of the carrier of t
x * n is Element of the carrier of t
1 - x is V24() real ext-real Element of REAL
(1 - x) * B is Element of the carrier of t
(x * n) + ((1 - x) * 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,(x * n),((1 - x) * B)) is Element of the carrier of t
t is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL t 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 t) is non empty set
K32( the carrier of (TOP-REAL t)) is set
s is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),s) is Element of K32( the carrier of (TOP-REAL t))
{ (- b₁) where b₁ is Element of the carrier of (TOP-REAL t) : b₁ in s } is set
n is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
B is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
x is V24() real ext-real set
x * n is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
1 - x is V24() real ext-real Element of REAL
(1 - x) * B is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(x * n) + ((1 - x) * B) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
the addF of (TOP-REAL t) is V12() V30(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)) Element of K32(K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)))
K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)) is set
K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)) is set
K32(K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t))) is set
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(x * n),((1 - x) * B)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
s1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
- s1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
s2 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
- s2 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
x * s2 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(1 - x) * s1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(x * s2) + ((1 - x) * s1) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(x * s2),((1 - x) * s1)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
- ((x * s2) + ((1 - x) * s1)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
- (x * s2) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(- (x * s2)) - ((1 - x) * s1) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
- ((1 - x) * s1) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(- (x * s2)) + (- ((1 - x) * s1)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(- (x * s2)),(- ((1 - x) * s1))) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
x * (- s2) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(x * (- s2)) + (- ((1 - x) * s1)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(x * (- s2)),(- ((1 - x) * s1))) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
t is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL t 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 t) is non empty set
K32( the carrier of (TOP-REAL t)) is set
s is Element of K32( the carrier of (TOP-REAL t))
n is Element of K32( the carrier of (TOP-REAL t))
s + n is Element of K32( the carrier of (TOP-REAL t))
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of (TOP-REAL t) : ( b₁ in s & b₂ in n ) } is set
((TOP-REAL t),s,n) is Element of K32( the carrier of (TOP-REAL t))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b₁,n) c= s } is set
B is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
x is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
s1 is V24() real ext-real set
s1 * B is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
1 - s1 is V24() real ext-real Element of REAL
(1 - s1) * x is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(s1 * B) + ((1 - s1) * x) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
the addF of (TOP-REAL t) is V12() V30(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)) Element of K32(K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)))
K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)) is set
K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)) is set
K32(K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t))) is set
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(s1 * B),((1 - s1) * x)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
s2 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
b2 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
s2 + b2 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),s2,b2) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
b1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
b1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
b1 + b1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),b1,b1) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
s1 * b1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(1 - s1) * s2 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(s1 * b1) + ((1 - s1) * s2) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(s1 * b1),((1 - s1) * s2)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
s1 * b1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(1 - s1) * b2 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(s1 * b1) + ((1 - s1) * b2) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(s1 * b1),((1 - s1) * b2)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((s1 * b1) + ((1 - s1) * s2)) + ((s1 * b1) + ((1 - s1) * b2)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),((s1 * b1) + ((1 - s1) * s2)),((s1 * b1) + ((1 - s1) * b2))) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
{ (b₁ + b₂) where b₁, b₂ is V40(t) V83() V126() Element of the carrier of (TOP-REAL t) : ( b₁ in s & b₂ in n ) } is set
((s1 * b1) + ((1 - s1) * s2)) + (s1 * b1) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),((s1 * b1) + ((1 - s1) * s2)),(s1 * b1)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(((s1 * b1) + ((1 - s1) * s2)) + (s1 * b1)) + ((1 - s1) * b2) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(((s1 * b1) + ((1 - s1) * s2)) + (s1 * b1)),((1 - s1) * b2)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(s1 * b1) + (s1 * b1) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(s1 * b1),(s1 * b1)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((s1 * b1) + (s1 * b1)) + ((1 - s1) * s2) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),((s1 * b1) + (s1 * b1)),((1 - s1) * s2)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(((s1 * b1) + (s1 * b1)) + ((1 - s1) * s2)) + ((1 - s1) * b2) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(((s1 * b1) + (s1 * b1)) + ((1 - s1) * s2)),((1 - s1) * b2)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((1 - s1) * s2) + ((1 - s1) * b2) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),((1 - s1) * s2),((1 - s1) * b2)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((s1 * b1) + (s1 * b1)) + (((1 - s1) * s2) + ((1 - s1) * b2)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),((s1 * b1) + (s1 * b1)),(((1 - s1) * s2) + ((1 - s1) * b2))) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
s1 * (b1 + b1) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(s1 * (b1 + b1)) + (((1 - s1) * s2) + ((1 - s1) * b2)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(s1 * (b1 + b1)),(((1 - s1) * s2) + ((1 - s1) * b2))) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
B is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
x is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
s1 is V24() real ext-real set
s1 * B is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
1 - s1 is V24() real ext-real Element of REAL
(1 - s1) * x is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(s1 * B) + ((1 - s1) * x) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
the addF of (TOP-REAL t) is V12() V30(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)) Element of K32(K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)))
K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)) is set
K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t)) is set
K32(K33(K33( the carrier of (TOP-REAL t), the carrier of (TOP-REAL t)), the carrier of (TOP-REAL t))) is set
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(s1 * B),((1 - s1) * x)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((TOP-REAL t),((s1 * B) + ((1 - s1) * x)),n) is Element of K32( the carrier of (TOP-REAL t))
{ (b₁ + ((s1 * B) + ((1 - s1) * x))) where b₁ is Element of the carrier of (TOP-REAL t) : b₁ in n } is set
s2 is set
b2 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
b2 + ((s1 * B) + ((1 - s1) * x)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),b2,((s1 * B) + ((1 - s1) * x))) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
b2 + B is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),b2,B) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((TOP-REAL t),B,n) is Element of K32( the carrier of (TOP-REAL t))
{ (b₁ + B) where b₁ is Element of the carrier of (TOP-REAL t) : b₁ in n } is set
b2 + x is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),b2,x) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
{ (b₁ + x) where b₁ is V40(t) V83() V126() Element of the carrier of (TOP-REAL t) : b₁ in n } is set
s1 * (b2 + B) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(1 - s1) * (b2 + x) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(s1 * (b2 + B)) + ((1 - s1) * (b2 + x)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(s1 * (b2 + B)),((1 - s1) * (b2 + x))) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
b1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((TOP-REAL t),b1,n) is Element of K32( the carrier of (TOP-REAL t))
{ (b₁ + b1) where b₁ is Element of the carrier of (TOP-REAL t) : b₁ in n } is set
b1 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((TOP-REAL t),b1,n) is Element of K32( the carrier of (TOP-REAL t))
{ (b₁ + b1) where b₁ is Element of the carrier of (TOP-REAL t) : b₁ in n } is set
s1 * b2 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(s1 * b2) + (s1 * B) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(s1 * b2),(s1 * B)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((s1 * b2) + (s1 * B)) + ((1 - s1) * (b2 + x)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),((s1 * b2) + (s1 * B)),((1 - s1) * (b2 + x))) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(1 - s1) * b2 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((1 - s1) * b2) + ((1 - s1) * x) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),((1 - s1) * b2),((1 - s1) * x)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((s1 * b2) + (s1 * B)) + (((1 - s1) * b2) + ((1 - s1) * x)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),((s1 * b2) + (s1 * B)),(((1 - s1) * b2) + ((1 - s1) * x))) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((s1 * b2) + (s1 * B)) + ((1 - s1) * b2) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),((s1 * b2) + (s1 * B)),((1 - s1) * b2)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(((s1 * b2) + (s1 * B)) + ((1 - s1) * b2)) + ((1 - s1) * x) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(((s1 * b2) + (s1 * B)) + ((1 - s1) * b2)),((1 - s1) * x)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
1 * b2 is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(1 * b2) - (s1 * b2) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
- (s1 * b2) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(1 * b2) + (- (s1 * b2)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(1 * b2),(- (s1 * b2))) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((s1 * b2) + (s1 * B)) + ((1 * b2) - (s1 * b2)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),((s1 * b2) + (s1 * B)),((1 * b2) - (s1 * b2))) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(((s1 * b2) + (s1 * B)) + ((1 * b2) - (s1 * b2))) + ((1 - s1) * x) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(((s1 * b2) + (s1 * B)) + ((1 * b2) - (s1 * b2))),((1 - s1) * x)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((s1 * b2) + (s1 * B)) + (1 * b2) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),((s1 * b2) + (s1 * B)),(1 * b2)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(((s1 * b2) + (s1 * B)) + (1 * b2)) - (s1 * b2) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(((s1 * b2) + (s1 * B)) + (1 * b2)) + (- (s1 * b2)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(((s1 * b2) + (s1 * B)) + (1 * b2)),(- (s1 * b2))) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((((s1 * b2) + (s1 * B)) + (1 * b2)) - (s1 * b2)) + ((1 - s1) * x) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),((((s1 * b2) + (s1 * B)) + (1 * b2)) - (s1 * b2)),((1 - s1) * x)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(s1 * B) + (1 * b2) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(s1 * B),(1 * b2)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((s1 * B) + (1 * b2)) + (s1 * b2) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),((s1 * B) + (1 * b2)),(s1 * b2)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(((s1 * B) + (1 * b2)) + (s1 * b2)) - (s1 * b2) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(((s1 * B) + (1 * b2)) + (s1 * b2)) + (- (s1 * b2)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(((s1 * B) + (1 * b2)) + (s1 * b2)),(- (s1 * b2))) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((((s1 * B) + (1 * b2)) + (s1 * b2)) - (s1 * b2)) + ((1 - s1) * x) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),((((s1 * B) + (1 * b2)) + (s1 * b2)) - (s1 * b2)),((1 - s1) * x)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
((s1 * B) + (1 * b2)) + ((1 - s1) * x) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),((s1 * B) + (1 * b2)),((1 - s1) * x)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
(1 * b2) + ((s1 * B) + ((1 - s1) * x)) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
K164( the carrier of (TOP-REAL t), the addF of (TOP-REAL t),(1 * b2),((s1 * B) + ((1 - s1) * x))) is V40(t) V83() V126() Element of the carrier of (TOP-REAL t)
t is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL t 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 t) is non empty set
K32( the carrier of (TOP-REAL t)) is set
s is Element of K32( the carrier of (TOP-REAL t))
n is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),s,n) is Element of K32( the carrier of (TOP-REAL t))
((TOP-REAL t),s,n) is Element of K32( the carrier of (TOP-REAL t))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b₁,n) c= s } is set
((TOP-REAL t),s,n) + n is Element of K32( the carrier of (TOP-REAL t))
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of (TOP-REAL t) : ( b₁ in ((TOP-REAL t),s,n) & b₂ in n ) } is set
((TOP-REAL t),s,n) is Element of K32( the carrier of (TOP-REAL t))
s + n is Element of K32( the carrier of (TOP-REAL t))
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of (TOP-REAL t) : ( b₁ in s & b₂ in n ) } is set
((TOP-REAL t),(s + n),n) is Element of K32( the carrier of (TOP-REAL t))
{ b₁ where b₁ is Element of the carrier of (TOP-REAL t) : ((TOP-REAL t),b₁,n) c= s + n } is set
t is V24() real ext-real set
s is V24() real ext-real set
s + t is V24() real ext-real set
n is natural V24() real ext-real V86() V87() V134() V135() V136() V137() V138() V139() Element of NAT
TOP-REAL n 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 n) is non empty set
K32( the carrier of (TOP-REAL n)) is set
B is Element of K32( the carrier of (TOP-REAL n))
((s + t),(TOP-REAL n),B) is Element of K32( the carrier of (TOP-REAL n))
{ ((s + t) * b₁) where b₁ is Element of the carrier of (TOP-REAL n) : b₁ in B } is set
(s,(TOP-REAL n),B) is Element of K32( the carrier of (TOP-REAL n))
{ (s * b₁) where b₁ is Element of the carrier of (TOP-REAL n) : b₁ in B } is set
(t,(TOP-REAL n),B) is Element of K32( the carrier of (TOP-REAL n))
{ (t * b₁) where b₁ is Element of the carrier of (TOP-REAL n) : b₁ in B } is set
(s,(TOP-REAL n),B) + (t,(TOP-REAL n),B) is Element of K32( the carrier of (TOP-REAL n))
{ (b₁ + b₂) where b₁, b₂ is Element of the carrier of (TOP-REAL n) : ( b₁ in (s,(TOP-REAL n),B) & b₂ in (t,(TOP-REAL n),B) ) } is set
x is set
s1 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
(s + t) * s1 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
t * s1 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
s * s1 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
(s * s1) + (t * s1) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) is V12() V30(K33( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n)) Element of K32(K33(K33( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n)))
K33( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)) is set
K33(K33( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n)) is set
K32(K33(K33( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n))) is set
K164( the carrier of (TOP-REAL n), the addF of (TOP-REAL n),(s * s1),(t * s1)) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
x is set
s1 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
s2 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
s1 + s2 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
the addF of (TOP-REAL n) is V12() V30(K33( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n)) Element of K32(K33(K33( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n)))
K33( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)) is set
K33(K33( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n)) is set
K32(K33(K33( the carrier of (TOP-REAL n), the carrier of (TOP-REAL n)), the carrier of (TOP-REAL n))) is set
K164( the carrier of (TOP-REAL n), the addF of (TOP-REAL n),s1,s2) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
b2 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
t * b2 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
b1 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
s * b1 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
(s + t) / (s + t) is V24() real ext-real set
s / (s + t) is V24() real ext-real set
(s / (s + t)) * b1 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
1 - (s / (s + t)) is V24() real ext-real Element of REAL
(1 - (s / (s + t))) * b2 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
((s / (s + t)) * b1) + ((1 - (s / (s + t))) * b2) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
K164( the carrier of (TOP-REAL n), the addF of (TOP-REAL n),((s / (s + t)) * b1),((1 - (s / (s + t))) * b2)) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
(s + t) * (((s / (s + t)) * b1) + ((1 - (s / (s + t))) * b2)) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
(s + t) * ((s / (s + t)) * b1) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
(s + t) * ((1 - (s / (s + t))) * b2) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
((s + t) * ((s / (s + t)) * b1)) + ((s + t) * ((1 - (s / (s + t))) * b2)) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
K164( the carrier of (TOP-REAL n), the addF of (TOP-REAL n),((s + t) * ((s / (s + t)) * b1)),((s + t) * ((1 - (s / (s + t))) * b2))) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
(s + t) * (s / (s + t)) is V24() real ext-real set
((s + t) * (s / (s + t))) * b1 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
(((s + t) * (s / (s + t))) * b1) + ((s + t) * ((1 - (s / (s + t))) * b2)) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
K164( the carrier of (TOP-REAL n), the addF of (TOP-REAL n),(((s + t) * (s / (s + t))) * b1),((s + t) * ((1 - (s / (s + t))) * b2))) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
(s + t) * (1 - (s / (s + t))) is V24() real ext-real Element of REAL
((s + t) * (1 - (s / (s + t)))) * b2 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
(((s + t) * (s / (s + t))) * b1) + (((s + t) * (1 - (s / (s + t)))) * b2) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
K164( the carrier of (TOP-REAL n), the addF of (TOP-REAL n),(((s + t) * (s / (s + t))) * b1),(((s + t) * (1 - (s / (s + t)))) * b2)) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
(s * b1) + (((s + t) * (1 - (s / (s + t)))) * b2) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
K164( the carrier of (TOP-REAL n), the addF of (TOP-REAL n),(s * b1),(((s + t) * (1 - (s / (s + t)))) * b2)) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
((s + t) / (s + t)) - (s / (s + t)) is V24() real ext-real set
(s + t) * (((s + t) / (s + t)) - (s / (s + t))) is V24() real ext-real set
((s + t) * (((s + t) / (s + t)) - (s / (s + t)))) * b2 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
(s * b1) + (((s + t) * (((s + t) / (s + t)) - (s / (s + t)))) * b2) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
K164( the carrier of (TOP-REAL n), the addF of (TOP-REAL n),(s * b1),(((s + t) * (((s + t) / (s + t)) - (s / (s + t)))) * b2)) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
(s + t) - s is V24() real ext-real set
((s + t) - s) / (s + t) is V24() real ext-real set
(s + t) * (((s + t) - s) / (s + t)) is V24() real ext-real set
((s + t) * (((s + t) - s) / (s + t))) * b2 is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
(s * b1) + (((s + t) * (((s + t) - s) / (s + t))) * b2) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)
K164( the carrier of (TOP-REAL n), the addF of (TOP-REAL n),(s * b1),(((s + t) * (((s + t) - s) / (s + t))) * b2)) is V40(n) V83() V126() Element of the carrier of (TOP-REAL n)