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<