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

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
is V40() V41() V42() set

omega is non empty epsilon-transitive epsilon-connected ordinal V59() V60() V61() V62() V63() V64() V65() set

{} is 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

rseq is set

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) + (n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() 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 [:[:(),():],():]
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

(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
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,():],():]

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

(nn) is V33() real ext-real Element of REAL

n1 is Element of ()

(n1) . nn is V33() real ext-real Element of REAL
rseq is Element of ()

n1 is Element of ()

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 ()

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) + (n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
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

(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
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) + (n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
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

((rseq + n1)) + (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool

(rseq) + (n1) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
(((rseq) + (n1))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
(((rseq) + (n1))) + (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
((rseq) + (n1)) + (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool

(rseq) + ((n1) + (nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
(((n1) + (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
(rseq) + (((n1) + (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
((n1 + nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
(rseq) + ((n1 + nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
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

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) + (- (n1)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool

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

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
rseq (#) ((n1 + nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool

(((n1) + (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
rseq (#) (((n1) + (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
rseq (#) ((n1) + (nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool

(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
((rseq * n1)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
((rseq * nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
((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
((rseq (#) (n1))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
((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
((rseq (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
((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
(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
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

(rseq + n1) (#) (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool

(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
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
((n1 * nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
((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
((rseq (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
((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
((n1 (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
((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
(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
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

(rseq * n1) (#) (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool

rseq (#) (n1 (#) (nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
((n1 (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
rseq (#) ((n1 (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
((n1 * nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
rseq (#) ((n1 * nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
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

() 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

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

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

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

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

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 set

() is Element of bool the carrier of ()
n1 is V33() real ext-real Element of REAL

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

((n1 * nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool

((n1 (#) (nn))) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
((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
(n1 (#) (nn)) (#) (nn) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
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
n1 (#) ((nn) (#) (nn)) is Relation-like NAT -defined REAL -valued Function-like non empty V14( NAT ) quasi_total V40() V41() V42() Element of bool
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
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

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<