:: RSSPACE semantic presentation

REAL is non empty V53() V59() V60() V61() V65() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V59() V60() V61() V62() V63() V64() V65() Element of bool REAL
bool REAL is set
COMPLEX is non empty V53() V59() V65() set
RAT is non empty V53() V59() V60() V61() V62() V65() set
INT is non empty V53() V59() V60() V61() V62() V63() V65() set
[:NAT,REAL:] is V40() V41() V42() set
bool [:NAT,REAL:] is set
omega is non empty epsilon-transitive epsilon-connected ordinal V59() V60() V61() V62() V63() V64() V65() set
bool omega is set
bool NAT is set
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V33() real ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V33() real ext-real positive non negative V38() V58() V59() V60() V61() V62() V63() V64() Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V38() V58() V59() V60() V61() V62() V63() V64() Element of NAT
Funcs (NAT,REAL) is functional non empty FUNCTION_DOMAIN of NAT , REAL
rseq is set
the Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:] is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
n1 is non empty set
nn is set
nn is set
u is set
rseq is non empty set
n1 is non empty set
nn is set
nn is set
() is non empty set
rseq is set
rseq is set
[:(),():] is set
[:[:(),():],():] is set
bool [:[:(),():],():] is set
rseq is Element of ()
n1 is Element of ()
(rseq) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq) + (n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq is Relation-like [:(),():] -defined () -valued Function-like V14([:(),():]) quasi_total Element of bool [:[:(),():],():]
rseq is Relation-like [:(),():] -defined () -valued Function-like V14([:(),():]) quasi_total Element of bool [:[:(),():],():]
rseq is Relation-like [:(),():] -defined () -valued Function-like V14([:(),():]) quasi_total Element of bool [:[:(),():],():]
n1 is Relation-like [:(),():] -defined () -valued Function-like V14([:(),():]) quasi_total Element of bool [:[:(),():],():]
() is Relation-like [:(),():] -defined () -valued Function-like V14([:(),():]) quasi_total Element of bool [:[:(),():],():]
[:REAL,():] is set
[:[:REAL,():],():] is set
bool [:[:REAL,():],():] is set
rseq is set
n1 is set
(n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq) is V33() real ext-real Element of REAL
(rseq) (#) (n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq is Relation-like [:REAL,():] -defined () -valued Function-like V14([:REAL,():]) quasi_total Element of bool [:[:REAL,():],():]
rseq is Relation-like [:REAL,():] -defined () -valued Function-like V14([:REAL,():]) quasi_total Element of bool [:[:REAL,():],():]
n1 is Relation-like [:REAL,():] -defined () -valued Function-like V14([:REAL,():]) quasi_total Element of bool [:[:REAL,():],():]
nn is V33() real ext-real Element of REAL
u is Element of ()
rseq . (nn,u) is Element of ()
[nn,u] is set
{nn,u} is set
{nn} is V59() V60() V61() set
{{nn,u},{nn}} is set
rseq . [nn,u] is set
n1 . (nn,u) is Element of ()
n1 . [nn,u] is set
(u) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(nn) is V33() real ext-real Element of REAL
(nn) (#) (u) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
() is Relation-like [:REAL,():] -defined () -valued Function-like V14([:REAL,():]) quasi_total Element of bool [:[:REAL,():],():]
NAT --> 0 is Relation-like NAT -defined NAT -valued RAT -valued INT -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() V43() Element of bool [:NAT,NAT:]
[:NAT,NAT:] is RAT -valued INT -valued V40() V41() V42() V43() set
bool [:NAT,NAT:] is set
rseq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
n1 is Element of ()
(n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
nn is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real set
(n1) . nn is V33() real ext-real Element of REAL
rseq is Element of ()
(rseq) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
n1 is Element of ()
(n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
nn is set
(rseq) . nn is V33() real ext-real Element of REAL
(n1) . nn is V33() real ext-real Element of REAL
() is Element of ()
rseq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
n1 is set
RLSStruct(# (),(),(),() #) is non empty strict RLSStruct
the carrier of RLSStruct(# (),(),(),() #) is non empty set
rseq is Element of the carrier of RLSStruct(# (),(),(),() #)
n1 is Element of the carrier of RLSStruct(# (),(),(),() #)
rseq + n1 is Element of the carrier of RLSStruct(# (),(),(),() #)
the addF of RLSStruct(# (),(),(),() #) is Relation-like [: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):] -defined the carrier of RLSStruct(# (),(),(),() #) -valued Function-like V14([: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):]
[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):] is set
[:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
bool [:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
the addF of RLSStruct(# (),(),(),() #) . (rseq,n1) is Element of the carrier of RLSStruct(# (),(),(),() #)
[rseq,n1] is set
{rseq,n1} is set
{rseq} is set
{{rseq,n1},{rseq}} is set
the addF of RLSStruct(# (),(),(),() #) . [rseq,n1] is set
(rseq) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq) + (n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq is V33() real ext-real Element of REAL
n1 is Element of the carrier of RLSStruct(# (),(),(),() #)
rseq * n1 is Element of the carrier of RLSStruct(# (),(),(),() #)
the Mult of RLSStruct(# (),(),(),() #) is Relation-like [:REAL, the carrier of RLSStruct(# (),(),(),() #):] -defined the carrier of RLSStruct(# (),(),(),() #) -valued Function-like V14([:REAL, the carrier of RLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[:REAL, the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):]
[:REAL, the carrier of RLSStruct(# (),(),(),() #):] is set
[:[:REAL, the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
bool [:[:REAL, the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
the Mult of RLSStruct(# (),(),(),() #) . (rseq,n1) is set
[rseq,n1] is set
{rseq,n1} is set
{rseq} is V59() V60() V61() set
{{rseq,n1},{rseq}} is set
the Mult of RLSStruct(# (),(),(),() #) . [rseq,n1] is set
(n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq (#) (n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq) is V33() real ext-real Element of REAL
(rseq) (#) (n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq is Element of the carrier of RLSStruct(# (),(),(),() #)
n1 is Element of the carrier of RLSStruct(# (),(),(),() #)
rseq + n1 is Element of the carrier of RLSStruct(# (),(),(),() #)
the addF of RLSStruct(# (),(),(),() #) is Relation-like [: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):] -defined the carrier of RLSStruct(# (),(),(),() #) -valued Function-like V14([: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):]
[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):] is set
[:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
bool [:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
the addF of RLSStruct(# (),(),(),() #) . (rseq,n1) is Element of the carrier of RLSStruct(# (),(),(),() #)
[rseq,n1] is set
{rseq,n1} is set
{rseq} is set
{{rseq,n1},{rseq}} is set
the addF of RLSStruct(# (),(),(),() #) . [rseq,n1] is set
n1 + rseq is Element of the carrier of RLSStruct(# (),(),(),() #)
the addF of RLSStruct(# (),(),(),() #) . (n1,rseq) is Element of the carrier of RLSStruct(# (),(),(),() #)
[n1,rseq] is set
{n1,rseq} is set
{n1} is set
{{n1,rseq},{n1}} is set
the addF of RLSStruct(# (),(),(),() #) . [n1,rseq] is set
(rseq) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq) + (n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq is Element of the carrier of RLSStruct(# (),(),(),() #)
n1 is Element of the carrier of RLSStruct(# (),(),(),() #)
rseq + n1 is Element of the carrier of RLSStruct(# (),(),(),() #)
the addF of RLSStruct(# (),(),(),() #) is Relation-like [: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):] -defined the carrier of RLSStruct(# (),(),(),() #) -valued Function-like V14([: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):]
[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):] is set
[:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
bool [:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
the addF of RLSStruct(# (),(),(),() #) . (rseq,n1) is Element of the carrier of RLSStruct(# (),(),(),() #)
[rseq,n1] is set
{rseq,n1} is set
{rseq} is set
{{rseq,n1},{rseq}} is set
the addF of RLSStruct(# (),(),(),() #) . [rseq,n1] is set
nn is Element of the carrier of RLSStruct(# (),(),(),() #)
(rseq + n1) + nn is Element of the carrier of RLSStruct(# (),(),(),() #)
the addF of RLSStruct(# (),(),(),() #) . ((rseq + n1),nn) is Element of the carrier of RLSStruct(# (),(),(),() #)
[(rseq + n1),nn] is set
{(rseq + n1),nn} is set
{(rseq + n1)} is set
{{(rseq + n1),nn},{(rseq + n1)}} is set
the addF of RLSStruct(# (),(),(),() #) . [(rseq + n1),nn] is set
n1 + nn is Element of the carrier of RLSStruct(# (),(),(),() #)
the addF of RLSStruct(# (),(),(),() #) . (n1,nn) is Element of the carrier of RLSStruct(# (),(),(),() #)
[n1,nn] is set
{n1,nn} is set
{n1} is set
{{n1,nn},{n1}} is set
the addF of RLSStruct(# (),(),(),() #) . [n1,nn] is set
rseq + (n1 + nn) is Element of the carrier of RLSStruct(# (),(),(),() #)
the addF of RLSStruct(# (),(),(),() #) . (rseq,(n1 + nn)) is Element of the carrier of RLSStruct(# (),(),(),() #)
[rseq,(n1 + nn)] is set
{rseq,(n1 + nn)} is set
{{rseq,(n1 + nn)},{rseq}} is set
the addF of RLSStruct(# (),(),(),() #) . [rseq,(n1 + nn)] is set
((rseq + n1)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((rseq + n1)) + (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq) + (n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(((rseq) + (n1))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(((rseq) + (n1))) + (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((rseq) + (n1)) + (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(n1) + (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq) + ((n1) + (nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(((n1) + (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq) + (((n1) + (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((n1 + nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq) + ((n1 + nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
0. RLSStruct(# (),(),(),() #) is V86( RLSStruct(# (),(),(),() #)) Element of the carrier of RLSStruct(# (),(),(),() #)
the ZeroF of RLSStruct(# (),(),(),() #) is Element of the carrier of RLSStruct(# (),(),(),() #)
n1 is Element of the carrier of RLSStruct(# (),(),(),() #)
n1 + (0. RLSStruct(# (),(),(),() #)) is Element of the carrier of RLSStruct(# (),(),(),() #)
the addF of RLSStruct(# (),(),(),() #) is Relation-like [: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):] -defined the carrier of RLSStruct(# (),(),(),() #) -valued Function-like V14([: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):]
[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):] is set
[:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
bool [:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
the addF of RLSStruct(# (),(),(),() #) . (n1,(0. RLSStruct(# (),(),(),() #))) is Element of the carrier of RLSStruct(# (),(),(),() #)
[n1,(0. RLSStruct(# (),(),(),() #))] is set
{n1,(0. RLSStruct(# (),(),(),() #))} is set
{n1} is set
{{n1,(0. RLSStruct(# (),(),(),() #))},{n1}} is set
the addF of RLSStruct(# (),(),(),() #) . [n1,(0. RLSStruct(# (),(),(),() #))] is set
(n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(()) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(n1) + (()) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
nn is set
((n1) + (())) . nn is V33() real ext-real Element of REAL
(n1) . nn is V33() real ext-real Element of REAL
(()) . nn is V33() real ext-real Element of REAL
((n1) . nn) + ((()) . nn) is V33() real ext-real Element of REAL
((n1) . nn) + 0 is V33() real ext-real Element of REAL
n1 is Element of the carrier of RLSStruct(# (),(),(),() #)
(n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
- (n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(n1) + (- (n1)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(()) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
u is set
((n1) + (- (n1))) . u is V33() real ext-real Element of REAL
(()) . u is V33() real ext-real Element of REAL
(n1) . u is V33() real ext-real Element of REAL
(- (n1)) . u is V33() real ext-real Element of REAL
((n1) . u) + ((- (n1)) . u) is V33() real ext-real Element of REAL
- ((n1) . u) is V33() real ext-real Element of REAL
((n1) . u) + (- ((n1) . u)) is V33() real ext-real Element of REAL
nn is Element of the carrier of RLSStruct(# (),(),(),() #)
n1 + nn is Element of the carrier of RLSStruct(# (),(),(),() #)
the addF of RLSStruct(# (),(),(),() #) is Relation-like [: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):] -defined the carrier of RLSStruct(# (),(),(),() #) -valued Function-like V14([: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):]
[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):] is set
[:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
bool [:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
the addF of RLSStruct(# (),(),(),() #) . (n1,nn) is Element of the carrier of RLSStruct(# (),(),(),() #)
[n1,nn] is set
{n1,nn} is set
{n1} is set
{{n1,nn},{n1}} is set
the addF of RLSStruct(# (),(),(),() #) . [n1,nn] is set
(nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(n1) + (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq is V33() real ext-real Element of REAL
n1 is Element of the carrier of RLSStruct(# (),(),(),() #)
nn is Element of the carrier of RLSStruct(# (),(),(),() #)
n1 + nn is Element of the carrier of RLSStruct(# (),(),(),() #)
the addF of RLSStruct(# (),(),(),() #) is Relation-like [: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):] -defined the carrier of RLSStruct(# (),(),(),() #) -valued Function-like V14([: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):]
[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):] is set
[:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
bool [:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
the addF of RLSStruct(# (),(),(),() #) . (n1,nn) is Element of the carrier of RLSStruct(# (),(),(),() #)
[n1,nn] is set
{n1,nn} is set
{n1} is set
{{n1,nn},{n1}} is set
the addF of RLSStruct(# (),(),(),() #) . [n1,nn] is set
rseq * (n1 + nn) is Element of the carrier of RLSStruct(# (),(),(),() #)
the Mult of RLSStruct(# (),(),(),() #) is Relation-like [:REAL, the carrier of RLSStruct(# (),(),(),() #):] -defined the carrier of RLSStruct(# (),(),(),() #) -valued Function-like V14([:REAL, the carrier of RLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[:REAL, the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):]
[:REAL, the carrier of RLSStruct(# (),(),(),() #):] is set
[:[:REAL, the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
bool [:[:REAL, the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
the Mult of RLSStruct(# (),(),(),() #) . (rseq,(n1 + nn)) is set
[rseq,(n1 + nn)] is set
{rseq,(n1 + nn)} is set
{rseq} is V59() V60() V61() set
{{rseq,(n1 + nn)},{rseq}} is set
the Mult of RLSStruct(# (),(),(),() #) . [rseq,(n1 + nn)] is set
rseq * n1 is Element of the carrier of RLSStruct(# (),(),(),() #)
the Mult of RLSStruct(# (),(),(),() #) . (rseq,n1) is set
[rseq,n1] is set
{rseq,n1} is set
{{rseq,n1},{rseq}} is set
the Mult of RLSStruct(# (),(),(),() #) . [rseq,n1] is set
rseq * nn is Element of the carrier of RLSStruct(# (),(),(),() #)
the Mult of RLSStruct(# (),(),(),() #) . (rseq,nn) is set
[rseq,nn] is set
{rseq,nn} is set
{{rseq,nn},{rseq}} is set
the Mult of RLSStruct(# (),(),(),() #) . [rseq,nn] is set
(rseq * n1) + (rseq * nn) is Element of the carrier of RLSStruct(# (),(),(),() #)
the addF of RLSStruct(# (),(),(),() #) . ((rseq * n1),(rseq * nn)) is Element of the carrier of RLSStruct(# (),(),(),() #)
[(rseq * n1),(rseq * nn)] is set
{(rseq * n1),(rseq * nn)} is set
{(rseq * n1)} is set
{{(rseq * n1),(rseq * nn)},{(rseq * n1)}} is set
the addF of RLSStruct(# (),(),(),() #) . [(rseq * n1),(rseq * nn)] is set
((n1 + nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq (#) ((n1 + nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(n1) + (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(((n1) + (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq (#) (((n1) + (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq (#) ((n1) + (nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq (#) (n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq (#) (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq (#) (n1)) + (rseq (#) (nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((rseq * n1)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((rseq * nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((rseq * n1)) + ((rseq * nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((rseq (#) (n1))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((rseq (#) (n1))) + ((rseq * nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((rseq (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((rseq (#) (n1))) + ((rseq (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq (#) (n1)) + ((rseq (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq is V33() real ext-real Element of REAL
n1 is V33() real ext-real Element of REAL
rseq + n1 is V33() real ext-real Element of REAL
nn is Element of the carrier of RLSStruct(# (),(),(),() #)
(rseq + n1) * nn is Element of the carrier of RLSStruct(# (),(),(),() #)
the Mult of RLSStruct(# (),(),(),() #) is Relation-like [:REAL, the carrier of RLSStruct(# (),(),(),() #):] -defined the carrier of RLSStruct(# (),(),(),() #) -valued Function-like V14([:REAL, the carrier of RLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[:REAL, the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):]
[:REAL, the carrier of RLSStruct(# (),(),(),() #):] is set
[:[:REAL, the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
bool [:[:REAL, the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
the Mult of RLSStruct(# (),(),(),() #) . ((rseq + n1),nn) is set
[(rseq + n1),nn] is set
{(rseq + n1),nn} is set
{(rseq + n1)} is V59() V60() V61() set
{{(rseq + n1),nn},{(rseq + n1)}} is set
the Mult of RLSStruct(# (),(),(),() #) . [(rseq + n1),nn] is set
rseq * nn is Element of the carrier of RLSStruct(# (),(),(),() #)
the Mult of RLSStruct(# (),(),(),() #) . (rseq,nn) is set
[rseq,nn] is set
{rseq,nn} is set
{rseq} is V59() V60() V61() set
{{rseq,nn},{rseq}} is set
the Mult of RLSStruct(# (),(),(),() #) . [rseq,nn] is set
n1 * nn is Element of the carrier of RLSStruct(# (),(),(),() #)
the Mult of RLSStruct(# (),(),(),() #) . (n1,nn) is set
[n1,nn] is set
{n1,nn} is set
{n1} is V59() V60() V61() set
{{n1,nn},{n1}} is set
the Mult of RLSStruct(# (),(),(),() #) . [n1,nn] is set
(rseq * nn) + (n1 * nn) is Element of the carrier of RLSStruct(# (),(),(),() #)
the addF of RLSStruct(# (),(),(),() #) is Relation-like [: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):] -defined the carrier of RLSStruct(# (),(),(),() #) -valued Function-like V14([: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):]
[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):] is set
[:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
bool [:[: the carrier of RLSStruct(# (),(),(),() #), the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
the addF of RLSStruct(# (),(),(),() #) . ((rseq * nn),(n1 * nn)) is Element of the carrier of RLSStruct(# (),(),(),() #)
[(rseq * nn),(n1 * nn)] is set
{(rseq * nn),(n1 * nn)} is set
{(rseq * nn)} is set
{{(rseq * nn),(n1 * nn)},{(rseq * nn)}} is set
the addF of RLSStruct(# (),(),(),() #) . [(rseq * nn),(n1 * nn)] is set
(nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq + n1) (#) (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq (#) (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
n1 (#) (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq (#) (nn)) + (n1 (#) (nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
u is set
((rseq + n1) (#) (nn)) . u is V33() real ext-real Element of REAL
((rseq (#) (nn)) + (n1 (#) (nn))) . u is V33() real ext-real Element of REAL
(nn) . u is V33() real ext-real Element of REAL
(rseq + n1) * ((nn) . u) is V33() real ext-real Element of REAL
rseq * ((nn) . u) is V33() real ext-real Element of REAL
n1 * ((nn) . u) is V33() real ext-real Element of REAL
(rseq * ((nn) . u)) + (n1 * ((nn) . u)) is V33() real ext-real Element of REAL
(rseq (#) (nn)) . u is V33() real ext-real Element of REAL
((rseq (#) (nn)) . u) + (n1 * ((nn) . u)) is V33() real ext-real Element of REAL
(n1 (#) (nn)) . u is V33() real ext-real Element of REAL
((rseq (#) (nn)) . u) + ((n1 (#) (nn)) . u) is V33() real ext-real Element of REAL
((rseq * nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((n1 * nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((rseq * nn)) + ((n1 * nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((rseq (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((rseq (#) (nn))) + ((n1 * nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((n1 (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((rseq (#) (nn))) + ((n1 (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq (#) (nn)) + ((n1 (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq is V33() real ext-real Element of REAL
n1 is V33() real ext-real Element of REAL
rseq * n1 is V33() real ext-real Element of REAL
nn is Element of the carrier of RLSStruct(# (),(),(),() #)
(rseq * n1) * nn is Element of the carrier of RLSStruct(# (),(),(),() #)
the Mult of RLSStruct(# (),(),(),() #) is Relation-like [:REAL, the carrier of RLSStruct(# (),(),(),() #):] -defined the carrier of RLSStruct(# (),(),(),() #) -valued Function-like V14([:REAL, the carrier of RLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[:REAL, the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):]
[:REAL, the carrier of RLSStruct(# (),(),(),() #):] is set
[:[:REAL, the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
bool [:[:REAL, the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
the Mult of RLSStruct(# (),(),(),() #) . ((rseq * n1),nn) is set
[(rseq * n1),nn] is set
{(rseq * n1),nn} is set
{(rseq * n1)} is V59() V60() V61() set
{{(rseq * n1),nn},{(rseq * n1)}} is set
the Mult of RLSStruct(# (),(),(),() #) . [(rseq * n1),nn] is set
n1 * nn is Element of the carrier of RLSStruct(# (),(),(),() #)
the Mult of RLSStruct(# (),(),(),() #) . (n1,nn) is set
[n1,nn] is set
{n1,nn} is set
{n1} is V59() V60() V61() set
{{n1,nn},{n1}} is set
the Mult of RLSStruct(# (),(),(),() #) . [n1,nn] is set
rseq * (n1 * nn) is Element of the carrier of RLSStruct(# (),(),(),() #)
the Mult of RLSStruct(# (),(),(),() #) . (rseq,(n1 * nn)) is set
[rseq,(n1 * nn)] is set
{rseq,(n1 * nn)} is set
{rseq} is V59() V60() V61() set
{{rseq,(n1 * nn)},{rseq}} is set
the Mult of RLSStruct(# (),(),(),() #) . [rseq,(n1 * nn)] is set
(nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(rseq * n1) (#) (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
n1 (#) (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq (#) (n1 (#) (nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((n1 (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq (#) ((n1 (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((n1 * nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq (#) ((n1 * nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
rseq is Element of the carrier of RLSStruct(# (),(),(),() #)
1 * rseq is Element of the carrier of RLSStruct(# (),(),(),() #)
the Mult of RLSStruct(# (),(),(),() #) is Relation-like [:REAL, the carrier of RLSStruct(# (),(),(),() #):] -defined the carrier of RLSStruct(# (),(),(),() #) -valued Function-like V14([:REAL, the carrier of RLSStruct(# (),(),(),() #):]) quasi_total Element of bool [:[:REAL, the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):]
[:REAL, the carrier of RLSStruct(# (),(),(),() #):] is set
[:[:REAL, the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
bool [:[:REAL, the carrier of RLSStruct(# (),(),(),() #):], the carrier of RLSStruct(# (),(),(),() #):] is set
the Mult of RLSStruct(# (),(),(),() #) . (1,rseq) is set
[1,rseq] is set
{1,rseq} is set
{1} is V59() V60() V61() V62() V63() V64() set
{{1,rseq},{1}} is set
the Mult of RLSStruct(# (),(),(),() #) . [1,rseq] is set
(rseq) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
1 (#) (rseq) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
() is RLSStruct
the carrier of () is non empty set
n1 is Element of the carrier of ()
nn is Element of the carrier of ()
n1 + nn is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V14([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set
the addF of () . (n1,nn) is Element of the carrier of ()
[n1,nn] is set
{n1,nn} is set
{n1} is set
{{n1,nn},{n1}} is set
the addF of () . [n1,nn] is set
u is Element of the carrier of ()
(n1 + nn) + u is Element of the carrier of ()
the addF of () . ((n1 + nn),u) is Element of the carrier of ()
[(n1 + nn),u] is set
{(n1 + nn),u} is set
{(n1 + nn)} is set
{{(n1 + nn),u},{(n1 + nn)}} is set
the addF of () . [(n1 + nn),u] is set
nn + u is Element of the carrier of ()
the addF of () . (nn,u) is Element of the carrier of ()
[nn,u] is set
{nn,u} is set
{nn} is set
{{nn,u},{nn}} is set
the addF of () . [nn,u] is set
n1 + (nn + u) is Element of the carrier of ()
the addF of () . (n1,(nn + u)) is Element of the carrier of ()
[n1,(nn + u)] is set
{n1,(nn + u)} is set
{{n1,(nn + u)},{n1}} is set
the addF of () . [n1,(nn + u)] is set
the carrier of () is non empty set
n1 is Element of the carrier of ()
0. () is V86(()) Element of the carrier of ()
the ZeroF of () is Element of the carrier of ()
n1 + (0. ()) is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V14([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set
the addF of () . (n1,(0. ())) is Element of the carrier of ()
[n1,(0. ())] is set
{n1,(0. ())} is set
{n1} is set
{{n1,(0. ())},{n1}} is set
the addF of () . [n1,(0. ())] is set
the carrier of () is non empty set
n1 is Element of the carrier of ()
0. () is V86(()) Element of the carrier of ()
the ZeroF of () is Element of the carrier of ()
the carrier of () is non empty set
n1 is V33() real ext-real set
nn is V33() real ext-real Element of REAL
u is Element of the carrier of ()
v is Element of the carrier of ()
u + v is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V14([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set
the addF of () . (u,v) is Element of the carrier of ()
[u,v] is set
{u,v} is set
{u} is set
{{u,v},{u}} is set
the addF of () . [u,v] is set
nn * (u + v) is Element of the carrier of ()
the Mult of () is Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V14([:REAL, the carrier of ():]) quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is set
[:[:REAL, the carrier of ():], the carrier of ():] is set
bool [:[:REAL, the carrier of ():], the carrier of ():] is set
the Mult of () . (nn,(u + v)) is set
[nn,(u + v)] is set
{nn,(u + v)} is set
{nn} is V59() V60() V61() set
{{nn,(u + v)},{nn}} is set
the Mult of () . [nn,(u + v)] is set
nn * u is Element of the carrier of ()
the Mult of () . (nn,u) is set
[nn,u] is set
{nn,u} is set
{{nn,u},{nn}} is set
the Mult of () . [nn,u] is set
nn * v is Element of the carrier of ()
the Mult of () . (nn,v) is set
[nn,v] is set
{nn,v} is set
{{nn,v},{nn}} is set
the Mult of () . [nn,v] is set
(nn * u) + (nn * v) is Element of the carrier of ()
the addF of () . ((nn * u),(nn * v)) is Element of the carrier of ()
[(nn * u),(nn * v)] is set
{(nn * u),(nn * v)} is set
{(nn * u)} is set
{{(nn * u),(nn * v)},{(nn * u)}} is set
the addF of () . [(nn * u),(nn * v)] is set
u is Element of the carrier of ()
v is Element of the carrier of ()
u + v is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V14([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set
the addF of () . (u,v) is Element of the carrier of ()
[u,v] is set
{u,v} is set
{u} is set
{{u,v},{u}} is set
the addF of () . [u,v] is set
n1 * (u + v) is Element of the carrier of ()
the Mult of () is Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V14([:REAL, the carrier of ():]) quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is set
[:[:REAL, the carrier of ():], the carrier of ():] is set
bool [:[:REAL, the carrier of ():], the carrier of ():] is set
the Mult of () . (n1,(u + v)) is set
[n1,(u + v)] is set
{n1,(u + v)} is set
{n1} is V59() V60() V61() set
{{n1,(u + v)},{n1}} is set
the Mult of () . [n1,(u + v)] is set
n1 * u is Element of the carrier of ()
the Mult of () . (n1,u) is set
[n1,u] is set
{n1,u} is set
{{n1,u},{n1}} is set
the Mult of () . [n1,u] is set
n1 * v is Element of the carrier of ()
the Mult of () . (n1,v) is set
[n1,v] is set
{n1,v} is set
{{n1,v},{n1}} is set
the Mult of () . [n1,v] is set
(n1 * u) + (n1 * v) is Element of the carrier of ()
the addF of () . ((n1 * u),(n1 * v)) is Element of the carrier of ()
[(n1 * u),(n1 * v)] is set
{(n1 * u),(n1 * v)} is set
{(n1 * u)} is set
{{(n1 * u),(n1 * v)},{(n1 * u)}} is set
the addF of () . [(n1 * u),(n1 * v)] is set
n1 is V33() real ext-real set
nn is V33() real ext-real set
n1 + nn is V33() real ext-real set
u is V33() real ext-real Element of REAL
v is V33() real ext-real Element of REAL
u + v is V33() real ext-real Element of REAL
w is Element of the carrier of ()
(u + v) * w is Element of the carrier of ()
the Mult of () is Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V14([:REAL, the carrier of ():]) quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is set
[:[:REAL, the carrier of ():], the carrier of ():] is set
bool [:[:REAL, the carrier of ():], the carrier of ():] is set
the Mult of () . ((u + v),w) is set
[(u + v),w] is set
{(u + v),w} is set
{(u + v)} is V59() V60() V61() set
{{(u + v),w},{(u + v)}} is set
the Mult of () . [(u + v),w] is set
u * w is Element of the carrier of ()
the Mult of () . (u,w) is set
[u,w] is set
{u,w} is set
{u} is V59() V60() V61() set
{{u,w},{u}} is set
the Mult of () . [u,w] is set
v * w is Element of the carrier of ()
the Mult of () . (v,w) is set
[v,w] is set
{v,w} is set
{v} is V59() V60() V61() set
{{v,w},{v}} is set
the Mult of () . [v,w] is set
(u * w) + (v * w) is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V14([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set
the addF of () . ((u * w),(v * w)) is Element of the carrier of ()
[(u * w),(v * w)] is set
{(u * w),(v * w)} is set
{(u * w)} is set
{{(u * w),(v * w)},{(u * w)}} is set
the addF of () . [(u * w),(v * w)] is set
w is Element of the carrier of ()
(n1 + nn) * w is Element of the carrier of ()
the Mult of () is Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V14([:REAL, the carrier of ():]) quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is set
[:[:REAL, the carrier of ():], the carrier of ():] is set
bool [:[:REAL, the carrier of ():], the carrier of ():] is set
the Mult of () . ((n1 + nn),w) is set
[(n1 + nn),w] is set
{(n1 + nn),w} is set
{(n1 + nn)} is V59() V60() V61() set
{{(n1 + nn),w},{(n1 + nn)}} is set
the Mult of () . [(n1 + nn),w] is set
n1 * w is Element of the carrier of ()
the Mult of () . (n1,w) is set
[n1,w] is set
{n1,w} is set
{n1} is V59() V60() V61() set
{{n1,w},{n1}} is set
the Mult of () . [n1,w] is set
nn * w is Element of the carrier of ()
the Mult of () . (nn,w) is set
[nn,w] is set
{nn,w} is set
{nn} is V59() V60() V61() set
{{nn,w},{nn}} is set
the Mult of () . [nn,w] is set
(n1 * w) + (nn * w) is Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V14([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set
the addF of () . ((n1 * w),(nn * w)) is Element of the carrier of ()
[(n1 * w),(nn * w)] is set
{(n1 * w),(nn * w)} is set
{(n1 * w)} is set
{{(n1 * w),(nn * w)},{(n1 * w)}} is set
the addF of () . [(n1 * w),(nn * w)] is set
n1 is V33() real ext-real set
nn is V33() real ext-real set
n1 * nn is V33() real ext-real set
u is V33() real ext-real Element of REAL
v is V33() real ext-real Element of REAL
u * v is V33() real ext-real Element of REAL
w is Element of the carrier of ()
(u * v) * w is Element of the carrier of ()
the Mult of () is Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V14([:REAL, the carrier of ():]) quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is set
[:[:REAL, the carrier of ():], the carrier of ():] is set
bool [:[:REAL, the carrier of ():], the carrier of ():] is set
the Mult of () . ((u * v),w) is set
[(u * v),w] is set
{(u * v),w} is set
{(u * v)} is V59() V60() V61() set
{{(u * v),w},{(u * v)}} is set
the Mult of () . [(u * v),w] is set
v * w is Element of the carrier of ()
the Mult of () . (v,w) is set
[v,w] is set
{v,w} is set
{v} is V59() V60() V61() set
{{v,w},{v}} is set
the Mult of () . [v,w] is set
u * (v * w) is Element of the carrier of ()
the Mult of () . (u,(v * w)) is set
[u,(v * w)] is set
{u,(v * w)} is set
{u} is V59() V60() V61() set
{{u,(v * w)},{u}} is set
the Mult of () . [u,(v * w)] is set
w is Element of the carrier of ()
(n1 * nn) * w is Element of the carrier of ()
the Mult of () is Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V14([:REAL, the carrier of ():]) quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is set
[:[:REAL, the carrier of ():], the carrier of ():] is set
bool [:[:REAL, the carrier of ():], the carrier of ():] is set
the Mult of () . ((n1 * nn),w) is set
[(n1 * nn),w] is set
{(n1 * nn),w} is set
{(n1 * nn)} is V59() V60() V61() set
{{(n1 * nn),w},{(n1 * nn)}} is set
the Mult of () . [(n1 * nn),w] is set
nn * w is Element of the carrier of ()
the Mult of () . (nn,w) is set
[nn,w] is set
{nn,w} is set
{nn} is V59() V60() V61() set
{{nn,w},{nn}} is set
the Mult of () . [nn,w] is set
n1 * (nn * w) is Element of the carrier of ()
the Mult of () . (n1,(nn * w)) is set
[n1,(nn * w)] is set
{n1,(nn * w)} is set
{n1} is V59() V60() V61() set
{{n1,(nn * w)},{n1}} is set
the Mult of () . [n1,(nn * w)] is set
n1 is Element of the carrier of ()
1 * n1 is Element of the carrier of ()
the Mult of () is Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V14([:REAL, the carrier of ():]) quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is set
[:[:REAL, the carrier of ():], the carrier of ():] is set
bool [:[:REAL, the carrier of ():], the carrier of ():] is set
the Mult of () . (1,n1) is set
[1,n1] is set
{1,n1} is set
{1} is V59() V60() V61() V62() V63() V64() set
{{1,n1},{1}} is set
the Mult of () . [1,n1] is set
rseq is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
the carrier of rseq is non empty set
bool the carrier of rseq is set
n1 is Element of bool the carrier of rseq
the addF of rseq is Relation-like [: the carrier of rseq, the carrier of rseq:] -defined the carrier of rseq -valued Function-like V14([: the carrier of rseq, the carrier of rseq:]) quasi_total Element of bool [:[: the carrier of rseq, the carrier of rseq:], the carrier of rseq:]
[: the carrier of rseq, the carrier of rseq:] is set
[:[: the carrier of rseq, the carrier of rseq:], the carrier of rseq:] is set
bool [:[: the carrier of rseq, the carrier of rseq:], the carrier of rseq:] is set
the addF of rseq || n1 is Relation-like Function-like set
[:n1,n1:] is set
the addF of rseq | [:n1,n1:] is Relation-like set
[:[:n1,n1:],n1:] is set
bool [:[:n1,n1:],n1:] is set
dom the addF of rseq is Relation-like set
nn is set
( the addF of rseq || n1) . nn is set
u is set
v is set
[u,v] is set
{u,v} is set
{u} is set
{{u,v},{u}} is set
dom ( the addF of rseq || n1) is set
u1 is left_complementable right_complementable complementable Element of the carrier of rseq
w is left_complementable right_complementable complementable Element of the carrier of rseq
u1 + w is left_complementable right_complementable complementable Element of the carrier of rseq
the addF of rseq . (u1,w) is left_complementable right_complementable complementable Element of the carrier of rseq
[u1,w] is set
{u1,w} is set
{u1} is set
{{u1,w},{u1}} is set
the addF of rseq . [u1,w] is set
dom ( the addF of rseq || n1) is set
rseq is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
the carrier of rseq is non empty set
bool the carrier of rseq is set
n1 is Element of bool the carrier of rseq
[:REAL, the carrier of rseq:] is set
the Mult of rseq is Relation-like [:REAL, the carrier of rseq:] -defined the carrier of rseq -valued Function-like V14([:REAL, the carrier of rseq:]) quasi_total Element of bool [:[:REAL, the carrier of rseq:], the carrier of rseq:]
[:[:REAL, the carrier of rseq:], the carrier of rseq:] is set
bool [:[:REAL, the carrier of rseq:], the carrier of rseq:] is set
[:REAL,n1:] is set
the Mult of rseq | [:REAL,n1:] is Relation-like [:REAL, the carrier of rseq:] -defined the carrier of rseq -valued Function-like Element of bool [:[:REAL, the carrier of rseq:], the carrier of rseq:]
[:[:REAL,n1:],n1:] is set
bool [:[:REAL,n1:],n1:] is set
dom the Mult of rseq is Relation-like set
nn is set
( the Mult of rseq | [:REAL,n1:]) . nn is set
u is set
v is set
[u,v] is set
{u,v} is set
{u} is set
{{u,v},{u}} is set
w is V33() real ext-real Element of REAL
[w,v] is set
{w,v} is set
{w} is V59() V60() V61() set
{{w,v},{w}} is set
dom ( the Mult of rseq | [:REAL,n1:]) is Relation-like set
u1 is left_complementable right_complementable complementable Element of the carrier of rseq
w * u1 is left_complementable right_complementable complementable Element of the carrier of rseq
the Mult of rseq . (w,u1) is set
[w,u1] is set
{w,u1} is set
{{w,u1},{w}} is set
the Mult of rseq . [w,u1] is set
dom ( the Mult of rseq | [:REAL,n1:]) is Relation-like set
rseq is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
the carrier of rseq is non empty set
bool the carrier of rseq is set
n1 is Element of bool the carrier of rseq
0. rseq is V86(rseq) left_complementable right_complementable complementable Element of the carrier of rseq
the ZeroF of rseq is left_complementable right_complementable complementable Element of the carrier of rseq
the Element of n1 is Element of n1
u is left_complementable right_complementable complementable Element of the carrier of rseq
u - u is left_complementable right_complementable complementable Element of the carrier of rseq
- u is left_complementable right_complementable complementable Element of the carrier of rseq
u + (- u) is left_complementable right_complementable complementable Element of the carrier of rseq
the addF of rseq is Relation-like [: the carrier of rseq, the carrier of rseq:] -defined the carrier of rseq -valued Function-like V14([: the carrier of rseq, the carrier of rseq:]) quasi_total Element of bool [:[: the carrier of rseq, the carrier of rseq:], the carrier of rseq:]
[: the carrier of rseq, the carrier of rseq:] is set
[:[: the carrier of rseq, the carrier of rseq:], the carrier of rseq:] is set
bool [:[: the carrier of rseq, the carrier of rseq:], the carrier of rseq:] is set
the addF of rseq . (u,(- u)) is left_complementable right_complementable complementable Element of the carrier of rseq
[u,(- u)] is set
{u,(- u)} is set
{u} is set
{{u,(- u)},{u}} is set
the addF of rseq . [u,(- u)] is set
rseq is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
the carrier of rseq is non empty set
bool the carrier of rseq is set
n1 is Element of bool the carrier of rseq
(rseq,n1) is Element of n1
(rseq,n1) is Relation-like [:n1,n1:] -defined n1 -valued Function-like quasi_total Element of bool [:[:n1,n1:],n1:]
[:n1,n1:] is set
[:[:n1,n1:],n1:] is set
bool [:[:n1,n1:],n1:] is set
(rseq,n1) is Relation-like [:REAL,n1:] -defined n1 -valued Function-like quasi_total Element of bool [:[:REAL,n1:],n1:]
[:REAL,n1:] is set
[:[:REAL,n1:],n1:] is set
bool [:[:REAL,n1:],n1:] is set
RLSStruct(# n1,(rseq,n1),(rseq,n1),(rseq,n1) #) is strict RLSStruct
[:REAL, the carrier of rseq:] is set
the Mult of rseq is Relation-like [:REAL, the carrier of rseq:] -defined the carrier of rseq -valued Function-like V14([:REAL, the carrier of rseq:]) quasi_total Element of bool [:[:REAL, the carrier of rseq:], the carrier of rseq:]
[:[:REAL, the carrier of rseq:], the carrier of rseq:] is set
bool [:[:REAL, the carrier of rseq:], the carrier of rseq:] is set
the Mult of rseq | [:REAL,n1:] is Relation-like [:REAL, the carrier of rseq:] -defined the carrier of rseq -valued Function-like Element of bool [:[:REAL, the carrier of rseq:], the carrier of rseq:]
0. rseq is V86(rseq) left_complementable right_complementable complementable Element of the carrier of rseq
the ZeroF of rseq is left_complementable right_complementable complementable Element of the carrier of rseq
the addF of rseq is Relation-like [: the carrier of rseq, the carrier of rseq:] -defined the carrier of rseq -valued Function-like V14([: the carrier of rseq, the carrier of rseq:]) quasi_total Element of bool [:[: the carrier of rseq, the carrier of rseq:], the carrier of rseq:]
[: the carrier of rseq, the carrier of rseq:] is set
[:[: the carrier of rseq, the carrier of rseq:], the carrier of rseq:] is set
bool [:[: the carrier of rseq, the carrier of rseq:], the carrier of rseq:] is set
the addF of rseq || n1 is Relation-like Function-like set
the addF of rseq | [:n1,n1:] is Relation-like set
the carrier of () is non empty set
bool the carrier of () is set
rseq is set
n1 is set
bool () is set
rseq is Element of bool the carrier of ()
n1 is Element of bool the carrier of ()
nn is set
(nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(nn) (#) (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
nn is set
(nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(nn) (#) (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
() is Element of bool the carrier of ()
n1 is V33() real ext-real Element of REAL
nn is left_complementable right_complementable complementable Element of the carrier of ()
n1 * nn is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () is Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V14([:REAL, the carrier of ():]) quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is set
[:[:REAL, the carrier of ():], the carrier of ():] is set
bool [:[:REAL, the carrier of ():], the carrier of ():] is set
the Mult of () . (n1,nn) is set
[n1,nn] is set
{n1,nn} is set
{n1} is V59() V60() V61() set
{{n1,nn},{n1}} is set
the Mult of () . [n1,nn] is set
(nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(nn) (#) (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((n1 * nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
n1 (#) (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((n1 (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((n1 * nn)) (#) ((n1 * nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(n1 (#) (nn)) (#) (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
n1 (#) ((n1 (#) (nn)) (#) (nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
n1 (#) ((nn) (#) (nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
n1 (#) (n1 (#) ((nn) (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
n1 * n1 is V33() real ext-real Element of REAL
(n1 * n1) (#) ((nn) (#) (nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
n1 is left_complementable right_complementable complementable Element of the carrier of ()
nn is left_complementable right_complementable complementable Element of the carrier of ()
n1 + nn is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V14([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set
the addF of () . (n1,nn) is left_complementable right_complementable complementable Element of the carrier of ()
[n1,nn] is set
{n1,nn} is set
{n1} is set
{{n1,nn},{n1}} is set
the addF of () . [n1,nn] is set
((n1 + nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((n1 + nn)) (#) ((n1 + nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(nn) (#) (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(n1) (#) (n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
u1 is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V38() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(((n1 + nn)) (#) ((n1 + nn))) . u1 is V33() real ext-real Element of REAL
((n1 + nn)) . u1 is V33() real ext-real Element of REAL
(((n1 + nn)) . u1) * (((n1 + nn)) . u1) is V33() real ext-real Element of REAL
2 is non empty epsilon-transitive epsilon-connected ordinal natural V33() real ext-real positive non negative V38() V58() V59() V60() V61() V62() V63() V64() Element of NAT
2 (#) ((n1) (#) (n1)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
2 (#) ((nn) (#) (nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(2 (#) ((n1) (#) (n1))) + (2 (#) ((nn) (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
w1 is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V38() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(((n1 + nn)) (#) ((n1 + nn))) . w1 is V33() real ext-real Element of REAL
((2 (#) ((n1) (#) (n1))) + (2 (#) ((nn) (#) (nn)))) . w1 is V33() real ext-real Element of REAL
(n1) . w1 is V33() real ext-real Element of REAL
(nn) . w1 is V33() real ext-real Element of REAL
(2 (#) ((n1) (#) (n1))) . w1 is V33() real ext-real Element of REAL
(2 (#) ((nn) (#) (nn))) . w1 is V33() real ext-real Element of REAL
((2 (#) ((n1) (#) (n1))) . w1) + ((2 (#) ((nn) (#) (nn))) . w1) is V33() real ext-real Element of REAL
((n1) (#) (n1)) . w1 is V33() real ext-real Element of REAL
2 * (((n1) (#) (n1)) . w1) is V33() real ext-real Element of REAL
(2 * (((n1) (#) (n1)) . w1)) + ((2 (#) ((nn) (#) (nn))) . w1) is V33() real ext-real Element of REAL
((nn) (#) (nn)) . w1 is V33() real ext-real Element of REAL
2 * (((nn) (#) (nn)) . w1) is V33() real ext-real Element of REAL
(2 * (((n1) (#) (n1)) . w1)) + (2 * (((nn) (#) (nn)) . w1)) is V33() real ext-real Element of REAL
((n1) . w1) * ((n1) . w1) is V33() real ext-real Element of REAL
2 * (((n1) . w1) * ((n1) . w1)) is V33() real ext-real Element of REAL
(2 * (((n1) . w1) * ((n1) . w1))) + (2 * (((nn) (#) (nn)) . w1)) is V33() real ext-real Element of REAL
sn is V33() real ext-real Element of REAL
sn ^2 is V33() real ext-real Element of REAL
sn * sn is V33() real ext-real set
2 * (sn ^2) is V33() real ext-real Element of REAL
tn is V33() real ext-real Element of REAL
tn ^2 is V33() real ext-real Element of REAL
tn * tn is V33() real ext-real set
2 * (tn ^2) is V33() real ext-real Element of REAL
(2 * (sn ^2)) + (2 * (tn ^2)) is V33() real ext-real Element of REAL
sn - tn is V33() real ext-real Element of REAL
(sn - tn) ^2 is V33() real ext-real Element of REAL
(sn - tn) * (sn - tn) is V33() real ext-real set
(n1) + (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(((n1) + (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
((n1 + nn)) . w1 is V33() real ext-real Element of REAL
(((n1 + nn)) . w1) * (((n1 + nn)) . w1) is V33() real ext-real Element of REAL
((n1) . w1) + ((nn) . w1) is V33() real ext-real Element of REAL
((n1) + (nn)) . w1 is V33() real ext-real Element of REAL
(((n1) . w1) + ((nn) . w1)) * (((n1) + (nn)) . w1) is V33() real ext-real Element of REAL
(((n1) . w1) + ((nn) . w1)) ^2 is V33() real ext-real Element of REAL
(((n1) . w1) + ((nn) . w1)) * (((n1) . w1) + ((nn) . w1)) is V33() real ext-real set
2 * sn is V33() real ext-real Element of REAL
(2 * sn) * tn is V33() real ext-real Element of REAL
(sn ^2) + ((2 * sn) * tn) is V33() real ext-real Element of REAL
((sn ^2) + ((2 * sn) * tn)) + (tn ^2) is V33() real ext-real Element of REAL
0 + ((((n1 + nn)) (#) ((n1 + nn))) . w1) is V33() real ext-real Element of REAL
(((2 (#) ((n1) (#) (n1))) + (2 (#) ((nn) (#) (nn)))) . w1) - ((((n1 + nn)) (#) ((n1 + nn))) . w1) is V33() real ext-real Element of REAL
((((2 (#) ((n1) (#) (n1))) + (2 (#) ((nn) (#) (nn)))) . w1) - ((((n1 + nn)) (#) ((n1 + nn))) . w1)) + ((((n1 + nn)) (#) ((n1 + nn))) . w1) is V33() real ext-real Element of REAL
(()) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(()) (#) (()) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
n1 is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
nn is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V38() V58() V59() V60() V61() V62() V63() V64() Element of NAT
n1 . nn is V33() real ext-real Element of REAL
(()) . nn is V33() real ext-real Element of REAL
((()) . nn) * ((()) . nn) is V33() real ext-real Element of REAL
((()) . nn) * 0 is V33() real ext-real Element of REAL
((),()) is Element of ()
((),()) is Relation-like [:(),():] -defined () -valued Function-like V14([:(),():]) quasi_total Element of bool [:[:(),():],():]
[:(),():] is set
[:[:(),():],():] is set
bool [:[:(),():],():] is set
((),()) is Relation-like [:REAL,():] -defined () -valued Function-like V14([:REAL,():]) quasi_total Element of bool [:[:REAL,():],():]
[:REAL,():] is set
[:[:REAL,():],():] is set
bool [:[:REAL,():],():] is set
RLSStruct(# (),((),()),((),()),((),()) #) is non empty strict RLSStruct
rseq is set
n1 is set
nn is left_complementable right_complementable complementable Element of the carrier of ()
(nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
u is left_complementable right_complementable complementable Element of the carrier of ()
v is left_complementable right_complementable complementable Element of the carrier of ()
u + v is left_complementable right_complementable complementable Element of the carrier of ()
the addF of () is Relation-like [: the carrier of (), the carrier of ():] -defined the carrier of () -valued Function-like V14([: the carrier of (), the carrier of ():]) quasi_total Element of bool [:[: the carrier of (), the carrier of ():], the carrier of ():]
[: the carrier of (), the carrier of ():] is set
[:[: the carrier of (), the carrier of ():], the carrier of ():] is set
bool [:[: the carrier of (), the carrier of ():], the carrier of ():] is set
the addF of () . (u,v) is left_complementable right_complementable complementable Element of the carrier of ()
[u,v] is set
{u,v} is set
{u} is set
{{u,v},{u}} is set
the addF of () . [u,v] is set
(u) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(v) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(u) + (v) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
u1 is left_complementable right_complementable complementable Element of the carrier of ()
w is V33() real ext-real Element of REAL
w * u1 is left_complementable right_complementable complementable Element of the carrier of ()
the Mult of () is Relation-like [:REAL, the carrier of ():] -defined the carrier of () -valued Function-like V14([:REAL, the carrier of ():]) quasi_total Element of bool [:[:REAL, the carrier of ():], the carrier of ():]
[:REAL, the carrier of ():] is set
[:[:REAL, the carrier of ():], the carrier of ():] is set
bool [:[:REAL, the carrier of ():], the carrier of ():] is set
the Mult of () . (w,u1) is set
[w,u1] is set
{w,u1} is set
{w} is V59() V60() V61() set
{{w,u1},{w}} is set
the Mult of () . [w,u1] is set
(u1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
w (#) (u1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
[:[:(),():],REAL:] is V40() V41() V42() set
bool [:[:(),():],REAL:] is set
n1 is set
nn is set
(n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(n1) (#) (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
Sum ((n1) (#) (nn)) is V33() real ext-real Element of REAL
n1 is Relation-like [:(),():] -defined REAL -valued Function-like V14([:(),():]) quasi_total V40() V41() V42() Element of bool [:[:(),():],REAL:]
n1 is Relation-like [:(),():] -defined REAL -valued Function-like V14([:(),():]) quasi_total V40() V41() V42() Element of bool [:[:(),():],REAL:]
nn is Relation-like [:(),():] -defined REAL -valued Function-like V14([:(),():]) quasi_total V40() V41() V42() Element of bool [:[:(),():],REAL:]
u is set
v is set
n1 . (u,v) is set
[u,v] is set
{u,v} is set
{u} is set
{{u,v},{u}} is set
n1 . [u,v] is V33() real ext-real set
nn . (u,v) is set
nn . [u,v] is V33() real ext-real set
(u) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(v) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
(u) (#) (v) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
Sum ((u) (#) (v)) is V33() real ext-real Element of REAL
() is Relation-like [:(),():] -defined REAL -valued Function-like V14([:(),():]) quasi_total V40() V41() V42() Element of bool [:[:(),():],REAL:]
UNITSTR(# (),((),()),((),()),((),()),() #) is non empty strict UNITSTR
() is non empty UNITSTR
rseq is RLSStruct
the carrier of rseq is set
the ZeroF of rseq is Element of the carrier of rseq
the addF of rseq is Relation-like [: the carrier of rseq, the carrier of rseq:] -defined the carrier of rseq -valued Function-like quasi_total Element of bool [:[: the carrier of rseq, the carrier of rseq:], the carrier of rseq:]
[: the carrier of rseq, the carrier of rseq:] is set
[:[: the carrier of rseq, the carrier of rseq:], the carrier of rseq:] is set
bool [:[: the carrier of rseq, the carrier of rseq:], the carrier of rseq:] is set
the Mult of rseq is Relation-like [:REAL, the carrier of rseq:] -defined the carrier of rseq -valued Function-like quasi_total Element of bool [:[:REAL, the carrier of rseq:], the carrier of rseq:]
[:REAL, the carrier of rseq:] is set
[:[:REAL, the carrier of rseq:], the carrier of rseq:] is set
bool [:[:REAL, the carrier of rseq:], the carrier of rseq:] is set
RLSStruct(# the carrier of rseq, the ZeroF of rseq, the addF of rseq, the Mult of rseq #) is strict RLSStruct
n1 is non empty RLSStruct
the carrier of n1 is non empty set
0. n1 is V86(n1) Element of the carrier of n1
the ZeroF of n1 is Element of the carrier of n1
the addF of n1 is Relation-like [: the carrier of n1, the carrier of n1:] -defined the carrier of n1 -valued Function-like V14([: the carrier of n1, the carrier of n1:]) quasi_total Element of bool [:[: the carrier of n1, the carrier of n1:], the carrier of n1:]
[: the carrier of n1, the carrier of n1:] is set
[:[: the carrier of n1, the carrier of n1:], the carrier of n1:] is set
bool [:[: the carrier of n1, the carrier of n1:], the carrier of n1:] is set
the Mult of n1 is Relation-like [:REAL, the carrier of n1:] -defined the carrier of n1 -valued Function-like V14([:REAL, the carrier of n1:]) quasi_total Element of bool [:[:REAL, the carrier of n1:], the carrier of n1:]
[:REAL, the carrier of n1:] is set
[:[:REAL, the carrier of n1:], the carrier of n1:] is set
bool [:[:REAL, the carrier of n1:], the carrier of n1:] is set
RLSStruct(# the carrier of n1,(0. n1), the addF of n1, the Mult of n1 #) is non empty strict RLSStruct
u is Element of the carrier of n1
v is Element of the carrier of n1
u + v is Element of the carrier of n1
the addF of n1 . (u,v) is Element of the carrier of n1
[u,v] is set
{u,v} is set
{u} is set
{{u,v},{u}} is set
the addF of n1 . [u,v] is set
v + u is Element of the carrier of n1
the addF of n1 . (v,u) is Element of the carrier of n1
[v,u] is set
{v,u} is set
{v} is set
{{v,u},{v}} is set
the addF of n1 . [v,u] is set
nn is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
the carrier of nn is non empty set
w is left_complementable right_complementable complementable Element of the carrier of nn
u1 is left_complementable right_complementable complementable Element of the carrier of nn
w + u1 is left_complementable right_complementable complementable Element of the carrier of nn
the addF of nn is Relation-like [: the carrier of nn, the carrier of nn:] -defined the carrier of nn -valued Function-like V14([: the carrier of nn, the carrier of nn:]) quasi_total Element of bool [:[: the carrier of nn, the carrier of nn:], the carrier of nn:]
[: the carrier of nn, the carrier of nn:] is set
[:[: the carrier of nn, the carrier of nn:], the carrier of nn:] is set
bool [:[: the carrier of nn, the carrier of nn:], the carrier of nn:] is set
the addF of nn . (w,u1) is left_complementable right_complementable complementable Element of the carrier of nn
[w,u1] is set
{w,u1} is set
{w} is set
{{w,u1},{w}} is set
the addF of nn . [w,u1] is set
u1 + w is left_complementable right_complementable complementable Element of the carrier of nn
the addF of nn . (u1,w) is left_complementable right_complementable complementable Element of the carrier of nn
[u1,w] is set
{u1,w} is set
{u1} is set
{{u1,w},{u1}} is set
the addF of nn . [u1,w] is set
u is Element of the carrier of n1
u + (0. n1) is Element of the carrier of n1
the addF of n1 . (u,(0. n1)) is Element of the carrier of n1
[u,(0. n1)] is set
{u,(0. n1)} is set
{u} is set
{{u,(0. n1)},{u}} is set
the addF of n1 . [u,(0. n1)] is set
nn is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
the carrier of nn is non empty set
v is left_complementable right_complementable complementable Element of the carrier of nn
0. nn is V86(nn) left_complementable right_complementable complementable Element of the carrier of nn
the ZeroF of nn is left_complementable right_complementable complementable Element of the carrier of nn
v + (0. nn) is left_complementable right_complementable complementable Element of the carrier of nn
the addF of nn is Relation-like [: the carrier of nn, the carrier of nn:] -defined the carrier of nn -valued Function-like V14([: the carrier of nn, the carrier of nn:]) quasi_total Element of bool [:[: the carrier of nn, the carrier of nn:], the carrier of nn:]
[: the carrier of nn, the carrier of nn:] is set
[:[: the carrier of nn, the carrier of nn:], the carrier of nn:] is set
bool [:[: the carrier of nn, the carrier of nn:], the carrier of nn:] is set
the addF of nn . (v,(0. nn)) is left_complementable right_complementable complementable Element of the carrier of nn
[v,(0. nn)] is set
{v,(0. nn)} is set
{v} is set
{{v,(0. nn)},{v}} is set
the addF of nn . [v,(0. nn)] is set
u is Element of the carrier of n1
nn is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
the carrier of nn is non empty set
v is left_complementable right_complementable complementable Element of the carrier of nn
0. nn is V86(nn) left_complementable right_complementable complementable Element of the carrier of nn
the ZeroF of nn is left_complementable right_complementable complementable Element of the carrier of nn
w is left_complementable right_complementable complementable Element of the carrier of nn
v + w is left_complementable right_complementable complementable Element of the carrier of nn
the addF of nn is Relation-like [: the carrier of nn, the carrier of nn:] -defined the carrier of nn -valued Function-like V14([: the carrier of nn, the carrier of nn:]) quasi_total Element of bool [:[: the carrier of nn, the carrier of nn:], the carrier of nn:]
[: the carrier of nn, the carrier of nn:] is set
[:[: the carrier of nn, the carrier of nn:], the carrier of nn:] is set
bool [:[: the carrier of nn, the carrier of nn:], the carrier of nn:] is set
the addF of nn . (v,w) is left_complementable right_complementable complementable Element of the carrier of nn
[v,w] is set
{v,w} is set
{v} is set
{{v,w},{v}} is set
the addF of nn . [v,w] is set
u1 is Element of the carrier of n1
u + u1 is Element of the carrier of n1
the addF of n1 . (u,u1) is Element of the carrier of n1
[u,u1] is set
{u,u1} is set
{u} is set
{{u,u1},{u}} is set
the addF of n1 . [u,u1] is set
u is Element of the carrier of n1
1 * u is Element of the carrier of n1
the Mult of n1 . (1,u) is set
[1,u] is set
{1,u} is set
{1} is V59() V60() V61() V62() V63() V64() set
{{1,u},{1}} is set
the Mult of n1 . [1,u] is set
nn is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
the carrier of nn is non empty set
v is left_complementable right_complementable complementable Element of the carrier of nn
1 * v is left_complementable right_complementable complementable Element of the carrier of nn
the Mult of nn is Relation-like [:REAL, the carrier of nn:] -defined the carrier of nn -valued Function-like V14([:REAL, the carrier of nn:]) quasi_total Element of bool [:[:REAL, the carrier of nn:], the carrier of nn:]
[:REAL, the carrier of nn:] is set
[:[:REAL, the carrier of nn:], the carrier of nn:] is set
bool [:[:REAL, the carrier of nn:], the carrier of nn:] is set
the Mult of nn . (1,v) is set
[1,v] is set
{1,v} is set
{{1,v},{1}} is set
the Mult of nn . [1,v] is set
u is V33() real ext-real set
v is V33() real ext-real set
u * v is V33() real ext-real set
w is Element of the carrier of n1
(u * v) * w is Element of the carrier of n1
the Mult of n1 . ((u * v),w) is set
[(u * v),w] is set
{(u * v),w} is set
{(u * v)} is V59() V60() V61() set
{{(u * v),w},{(u * v)}} is set
the Mult of n1 . [(u * v),w] is set
v * w is Element of the carrier of n1
the Mult of n1 . (v,w) is set
[v,w] is set
{v,w} is set
{v} is V59() V60() V61() set
{{v,w},{v}} is set
the Mult of n1 . [v,w] is set
u * (v * w) is Element of the carrier of n1
the Mult of n1 . (u,(v * w)) is set
[u,(v * w)] is set
{u,(v * w)} is set
{u} is V59() V60() V61() set
{{u,(v * w)},{u}} is set
the Mult of n1 . [u,(v * w)] is set
nn is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
the carrier of nn is non empty set
u1 is left_complementable right_complementable complementable Element of the carrier of nn
(u * v) * u1 is left_complementable right_complementable complementable Element of the carrier of nn
the Mult of nn is Relation-like [:REAL, the carrier of nn:] -defined the carrier of nn -valued Function-like V14([:REAL, the carrier of nn:]) quasi_total Element of bool [:[:REAL, the carrier of nn:], the carrier of nn:]
[:REAL, the carrier of nn:] is set
[:[:REAL, the carrier of nn:], the carrier of nn:] is set
bool [:[:REAL, the carrier of nn:], the carrier of nn:] is set
the Mult of nn . ((u * v),u1) is set
[(u * v),u1] is set
{(u * v),u1} is set
{{(u * v),u1},{(u * v)}} is set
the Mult of nn . [(u * v),u1] is set
v * u1 is left_complementable right_complementable complementable Element of the carrier of nn
the Mult of nn . (v,u1) is set
[v,u1] is set
{v,u1} is set
{{v,u1},{v}} is set
the Mult of nn . [v,u1] is set
u * (v * u1) is left_complementable right_complementable complementable Element of the carrier of nn
the Mult of nn . (u,(v * u1)) is set
[u,(v * u1)] is set
{u,(v * u1)} is set
{{u,(v * u1)},{u}} is set
the Mult of nn . [u,(v * u1)] is set
u is V33() real ext-real set
v is V33() real ext-real set
u + v is V33() real ext-real set
w is Element of the carrier of n1
(u + v) * w is Element of the carrier of n1
the Mult of n1 . ((u + v),w) is set
[(u + v),w] is set
{(u + v),w} is set
{(u + v)} is V59() V60() V61() set
{{(u + v),w},{(u + v)}} is set
the Mult of n1 . [(u + v),w] is set
u * w is Element of the carrier of n1
the Mult of n1 . (u,w) is set
[u,w] is set
{u,w} is set
{u} is V59() V60() V61() set
{{u,w},{u}} is set
the Mult of n1 . [u,w] is set
v * w is Element of the carrier of n1
the Mult of n1 . (v,w) is set
[v,w] is set
{v,w} is set
{v} is V59() V60() V61() set
{{v,w},{v}} is set
the Mult of n1 . [v,w] is set
(u * w) + (v * w) is Element of the carrier of n1
the addF of n1 . ((u * w),(v * w)) is Element of the carrier of n1
[(u * w),(v * w)] is set
{(u * w),(v * w)} is set
{(u * w)} is set
{{(u * w),(v * w)},{(u * w)}} is set
the addF of n1 . [(u * w),(v * w)] is set
nn is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
the carrier of nn is non empty set
u1 is left_complementable right_complementable complementable Element of the carrier of nn
(u + v) * u1 is left_complementable right_complementable complementable Element of the carrier of nn
the Mult of nn is Relation-like [:REAL, the carrier of nn:] -defined the carrier of nn -valued Function-like V14([:REAL, the carrier of nn:]) quasi_total Element of bool [:[:REAL, the carrier of nn:], the carrier of nn:]
[:REAL, the carrier of nn:] is set
[:[:REAL, the carrier of nn:], the carrier of nn:] is set
bool [:[:REAL, the carrier of nn:], the carrier of nn:] is set
the Mult of nn . ((u + v),u1) is set
[(u + v),u1] is set
{(u + v),u1} is set
{{(u + v),u1},{(u + v)}} is set
the Mult of nn . [(u + v),u1] is set
u * u1 is left_complementable right_complementable complementable Element of the carrier of nn
the Mult of nn . (u,u1) is set
[u,u1] is set
{u,u1} is set
{{u,u1},{u}} is set
the Mult of nn . [u,u1] is set
v * u1 is left_complementable right_complementable complementable Element of the carrier of nn
the Mult of nn . (v,u1) is set
[v,u1] is set
{v,u1} is set
{{v,u1},{v}} is set
the Mult of nn . [v,u1] is set
(u * u1) + (v * u1) is left_complementable right_complementable complementable Element of the carrier of nn
the addF of nn is Relation-like [: the carrier of nn, the carrier of nn:] -defined the carrier of nn -valued Function-like V14([: the carrier of nn, the carrier of nn:]) quasi_total Element of bool [:[: the carrier of nn, the carrier of nn:], the carrier of nn:]
[: the carrier of nn, the carrier of nn:] is set
[:[: the carrier of nn, the carrier of nn:], the carrier of nn:] is set
bool [:[: the carrier of nn, the carrier of nn:], the carrier of nn:] is set
the addF of nn . ((u * u1),(v * u1)) is left_complementable right_complementable complementable Element of the carrier of nn
[(u * u1),(v * u1)] is set
{(u * u1),(v * u1)} is set
{(u * u1)} is set
{{(u * u1),(v * u1)},{(u * u1)}} is set
the addF of nn . [(u * u1),(v * u1)] is set
u is V33() real ext-real set
v is Element of the carrier of n1
w is Element of the carrier of n1
v + w is Element of the carrier of n1
the addF of n1 . (v,w) is Element of the carrier of n1
[v,w] is set
{v,w} is set
{v} is set
{{v,w},{v}} is set
the addF of n1 . [v,w] is set
u * (v + w) is Element of the carrier of n1
the Mult of n1 . (u,(v + w)) is set
[u,(v + w)] is set
{u,(v + w)} is set
{u} is V59() V60() V61() set
{{u,(v + w)},{u}} is set
the Mult of n1 . [u,(v + w)] is set
u * v is Element of the carrier of n1
the Mult of n1 . (u,v) is set
[u,v] is set
{u,v} is set
{{u,v},{u}} is set
the Mult of n1 . [u,v] is set
u * w is Element of the carrier of n1
the Mult of n1 . (u,w) is set
[u,w] is set
{u,w} is set
{{u,w},{u}} is set
the Mult of n1 . [u,w] is set
(u * v) + (u * w) is Element of the carrier of n1
the addF of n1 . ((u * v),(u * w)) is Element of the carrier of n1
[(u * v),(u * w)] is set
{(u * v),(u * w)} is set
{(u * v)} is set
{{(u * v),(u * w)},{(u * v)}} is set
the addF of n1 . [(u * v),(u * w)] is set
nn is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
the carrier of nn is non empty set
u1 is left_complementable right_complementable complementable Element of the carrier of nn
v1 is left_complementable right_complementable complementable Element of the carrier of nn
u1 + v1 is left_complementable right_complementable complementable Element of the carrier of nn
the addF of nn is Relation-like [: the carrier of nn, the carrier of nn:] -defined the carrier of nn -valued Function-like V14([: the carrier of nn, the carrier of nn:]) quasi_total Element of bool [:[: the carrier of nn, the carrier of nn:], the carrier of nn:]
[: the carrier of nn, the carrier of nn:] is set
[:[: the carrier of nn, the carrier of nn:], the carrier of nn:] is set
bool [:[: the carrier of nn, the carrier of nn:], the carrier of nn:] is set
the addF of nn . (u1,v1) is left_complementable right_complementable complementable Element of the carrier of nn
[u1,v1] is set
{u1,v1} is set
{u1} is set
{{u1,v1},{u1}} is set
the addF of nn . [u1,v1] is set
u * (u1 + v1) is left_complementable right_complementable complementable Element of the carrier of nn
the Mult of nn is Relation-like [:REAL, the carrier of nn:] -defined the carrier of nn -valued Function-like V14([:REAL, the carrier of nn:]) quasi_total Element of bool [:[:REAL, the carrier of nn:], the carrier of nn:]
[:REAL, the carrier of nn:] is set
[:[:REAL, the carrier of nn:], the carrier of nn:] is set
bool [:[:REAL, the carrier of nn:], the carrier of nn:] is set
the Mult of nn . (u,(u1 + v1)) is set
[u,(u1 + v1)] is set
{u,(u1 + v1)} is set
{{u,(u1 + v1)},{u}} is set
the Mult of nn . [u,(u1 + v1)] is set
u * u1 is left_complementable right_complementable complementable Element of the carrier of nn
the Mult of nn . (u,u1) is set
[u,u1] is set
{u,u1} is set
{{u,u1},{u}} is set
the Mult of nn . [u,u1] is set
u * v1 is left_complementable right_complementable complementable Element of the carrier of nn
the Mult of nn . (u,v1) is set
[u,v1] is set
{u,v1} is set
{{u,v1},{u}} is set
the Mult of nn . [u,v1] is set
(u * u1) + (u * v1) is left_complementable right_complementable complementable Element of the carrier of nn
the addF of nn . ((u * u1),(u * v1)) is left_complementable right_complementable complementable Element of the carrier of nn
[(u * u1),(u * v1)] is set
{(u * u1),(u * v1)} is set
{(u * u1)} is set
{{(u * u1),(u * v1)},{(u * u1)}} is set
the addF of nn . [(u * u1),(u * v1)] is set
u is Element of the carrier of n1
v is Element of the carrier of n1
u + v is Element of the carrier of n1
the addF of n1 . (u,v) is Element of the carrier of n1
[u,v] is set
{u,v} is set
{u} is set
{{u,v},{u}} is set
the addF of n1 . [u,v] is set
w is Element of the carrier of n1
(u + v) + w is Element of the carrier of n1
the addF of n1 . ((u + v),w) is Element of the carrier of n1
[(u + v),w] is set
{(u + v),w} is set
{(u + v)} is set
{{(u + v),w},{(u + v)}} is set
the addF of n1 . [(u + v),w] is set
v + w is Element of the carrier of n1
the addF of n1 . (v,w) is Element of the carrier of n1
[v,w] is set
{v,w} is set
{v} is set
{{v,w},{v}} is set
the addF of n1 . [v,w] is set
u + (v + w) is Element of the carrier of n1
the addF of n1 . (u,(v + w)) is Element of the carrier of n1
[u,(v + w)] is set
{u,(v + w)} is set
{{u,(v + w)},{u}} is set
the addF of n1 . [u,(v + w)] is set
nn is non empty left_complementable right_complementable complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
the carrier of nn is non empty set
u1 is left_complementable right_complementable complementable Element of the carrier of nn
v1 is left_complementable right_complementable complementable Element of the carrier of nn
u1 + v1 is left_complementable right_complementable complementable Element of the carrier of nn
the addF of nn is Relation-like [: the carrier of nn, the carrier of nn:] -defined the carrier of nn -valued Function-like V14([: the carrier of nn, the carrier of nn:]) quasi_total Element of bool [:[: the carrier of nn, the carrier of nn:], the carrier of nn:]
[: the carrier of nn, the carrier of nn:] is set
[:[: the carrier of nn, the carrier of nn:], the carrier of nn:] is set
bool [:[: the carrier of nn, the carrier of nn:], the carrier of nn:] is set
the addF of nn . (u1,v1) is left_complementable right_complementable complementable Element of the carrier of nn
[u1,v1] is set
{u1,v1} is set
{u1} is set
{{u1,v1},{u1}} is set
the addF of nn . [u1,v1] is set
w1 is left_complementable right_complementable complementable Element of the carrier of nn
(u1 + v1) + w1 is left_complementable right_complementable complementable Element of the carrier of nn
the addF of nn . ((u1 + v1),w1) is left_complementable right_complementable complementable Element of the carrier of nn
[(u1 + v1),w1] is set
{(u1 + v1),w1} is set
{(u1 + v1)} is set
{{(u1 + v1),w1},{(u1 + v1)}} is set
the addF of nn . [(u1 + v1),w1] is set
v1 + w1 is left_complementable right_complementable complementable Element of the carrier of nn
the addF of nn . (v1,w1) is left_complementable right_complementable complementable Element of the carrier of nn
[v1,w1] is set
{v1,w1} is set
{v1} is set
{{v1,w1},{v1}} is set
the addF of nn . [v1,w1] is set
u1 + (v1 + w1) is left_complementable right_complementable complementable Element of the carrier of nn
the addF of nn . (u1,(v1 + w1)) is left_complementable right_complementable complementable Element of the carrier of nn
[u1,(v1 + w1)] is set
{u1,(v1 + w1)} is set
{{u1,(v1 + w1)},{u1}} is set
the addF of nn . [u1,(v1 + w1)] is set
rseq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
Sum rseq is V33() real ext-real Element of REAL
Partial_Sums rseq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
n1 is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V38() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums rseq) . n1 is V33() real ext-real Element of REAL
nn is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V38() V58() V59() V60() V61() V62() V63() V64() Element of NAT
rseq . nn is V33() real ext-real Element of REAL
(Partial_Sums rseq) . nn is V33() real ext-real Element of REAL
nn + 1 is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V38() V58() V59() V60() V61() V62() V63() V64() Element of NAT
rseq . (nn + 1) is V33() real ext-real Element of REAL
(Partial_Sums rseq) . (nn + 1) is V33() real ext-real Element of REAL
0 + (rseq . (nn + 1)) is V33() real ext-real Element of REAL
(rseq . nn) + (rseq . (nn + 1)) is V33() real ext-real Element of REAL
rseq . 0 is V33() real ext-real Element of REAL
(Partial_Sums rseq) . 0 is V33() real ext-real Element of REAL
rseq . n1 is V33() real ext-real Element of REAL
n1 is V33() real ext-real set
nn is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V38() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums rseq) . nn is V33() real ext-real Element of REAL
((Partial_Sums rseq) . nn) - 0 is V33() real ext-real Element of REAL
abs (((Partial_Sums rseq) . nn) - 0) is V33() real ext-real Element of REAL
0 - 0 is V33() real ext-real Element of REAL
abs (0 - 0) is V33() real ext-real Element of REAL
lim (Partial_Sums rseq) is V33() real ext-real Element of REAL
rseq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
Sum rseq is V33() real ext-real Element of REAL
Partial_Sums rseq is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool [:NAT,REAL:]
n1 is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real set
(Partial_Sums rseq) . n1 is V33() real ext-real Element of REAL
lim (Partial_Sums rseq) is V33() real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V38() V58() V59() V60() V61() V62() V63() V64() Element of NAT
rseq . n1 is V33() real ext-real Element of REAL
nn is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V38() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums rseq) . nn is V33() real ext-real Element of REAL
nn + 0 is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V38() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums rseq) . 0 is V33() real ext-real Element of REAL
rseq . 0 is V33() real ext-real Element of REAL
(Partial_Sums rseq) . n1 is V33() real ext-real Element of REAL
rseq . 0 is V33() real ext-real Element of REAL
n1 - 1 is V33() real ext-real Element of REAL
(n1 - 1) + 1 is V33() real ext-real Element of REAL
0 + 1 is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V38() V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums rseq) . (n1 - 1) is V33() real ext-real Element of REAL
(rseq . n1) + 0 is V33() real ext-real Element of REAL
(rseq . n1) + ((Partial_Sums rseq) . (n1 - 1)) is V33() real ext-real Element of REAL
n1 is epsilon-transitive epsilon-connected ordinal natural V33() real ext-real V38() V58() V59() V60() V61() V62() V63() V64() Element of NAT
rseq . n1 is V33() real ext-real Element of REAL