REAL is non empty V34() V144() V145() V146() V150() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V144() V145() V146() V147() V148() V149() V150() Element of bool REAL
bool REAL is non empty set
{} is empty Function-like functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V144() V145() V146() V147() V148() V149() V150() set
1 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V31() real V113() V114() V144() V145() V146() V147() V148() V149() Element of NAT
{{},1} is non empty V144() V145() V146() V147() V148() V149() set
INT is non empty V34() V144() V145() V146() V147() V148() V150() set
COMPLEX is non empty V34() V144() V150() set
omega is non empty epsilon-transitive epsilon-connected ordinal V144() V145() V146() V147() V148() V149() V150() set
bool omega is non empty set
bool NAT is non empty set
RAT is non empty V34() V144() V145() V146() V147() V150() set
[:REAL,REAL:] is non empty V134() V135() V136() set
bool [:REAL,REAL:] is non empty set
K392() is non empty strict multMagma
the carrier of K392() is non empty set
<REAL,+> is non empty strict V115() V116() associative commutative left-invertible right-invertible invertible left-cancelable right-cancelable V171() multMagma
K398() is non empty strict associative commutative left-cancelable right-cancelable V171() SubStr of <REAL,+>
<NAT,+> is non empty strict V115() associative commutative left-cancelable right-cancelable V171() uniquely-decomposable SubStr of K398()
<REAL,*> is non empty strict V115() associative commutative multMagma
<NAT,*> is non empty strict V115() associative commutative uniquely-decomposable SubStr of <REAL,*>
ExtREAL is non empty V145() set
[:NAT,REAL:] is non empty V134() V135() V136() set
bool [:NAT,REAL:] is non empty set
the_set_of_RealSequences is non empty set
[:the_set_of_RealSequences,the_set_of_RealSequences:] is non empty set
[:[:the_set_of_RealSequences,the_set_of_RealSequences:],the_set_of_RealSequences:] is non empty set
bool [:[:the_set_of_RealSequences,the_set_of_RealSequences:],the_set_of_RealSequences:] is non empty set
[:REAL,the_set_of_RealSequences:] is non empty set
[:[:REAL,the_set_of_RealSequences:],the_set_of_RealSequences:] is non empty set
bool [:[:REAL,the_set_of_RealSequences:],the_set_of_RealSequences:] is non empty set
Linear_Space_of_RealSequences is RLSStruct
the carrier of Linear_Space_of_RealSequences is set
bool the carrier of Linear_Space_of_RealSequences is non empty set
the_set_of_l2RealSequences is Element of bool the carrier of Linear_Space_of_RealSequences
[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:] is set
[:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL:] is V134() V135() V136() set
bool [:[:the_set_of_l2RealSequences,the_set_of_l2RealSequences:],REAL:] is non empty set
the_set_of_l1RealSequences is non empty linearly-closed Element of bool the carrier of Linear_Space_of_RealSequences
[:the_set_of_l1RealSequences,REAL:] is non empty V134() V135() V136() set
bool [:the_set_of_l1RealSequences,REAL:] is non empty set
[:COMPLEX,COMPLEX:] is non empty V134() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is non empty V134() V135() V136() set
bool [:COMPLEX,REAL:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V134() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty V134() V135() V136() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is non empty RAT -valued V134() V135() V136() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty RAT -valued V134() V135() V136() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty RAT -valued INT -valued V134() V135() V136() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty RAT -valued INT -valued V134() V135() V136() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty RAT -valued INT -valued V134() V135() V136() V137() set
[:[:NAT,NAT:],NAT:] is non empty RAT -valued INT -valued V134() V135() V136() V137() set
bool [:[:NAT,NAT:],NAT:] is non empty set
0 is empty Function-like functional ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V31() real V113() V114() V144() V145() V146() V147() V148() V149() V150() Element of NAT
- 1 is ext-real non positive V31() real Element of REAL
l1_Space is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V104() discerning reflexive RealNormSpace-like NORMSTR
the carrier of l1_Space is non empty set
[:NAT, the carrier of l1_Space:] is non empty set
bool [:NAT, the carrier of l1_Space:] is non empty set
2 is non empty ext-real positive non negative epsilon-transitive epsilon-connected ordinal natural V31() real V113() V114() V144() V145() V146() V147() V148() V149() Element of NAT
Y is non empty set
[:REAL,Y:] is non empty set
[:[:REAL,Y:],Y:] is non empty set
bool [:[:REAL,Y:],Y:] is non empty set
X is set
[:X,Y:] is set
bool [:X,Y:] is non empty set
vseq is non empty Relation-like [:REAL,Y:] -defined Y -valued Function-like total quasi_total Element of bool [:[:REAL,Y:],Y:]
f is ext-real V31() real set
tseq is Relation-like X -defined Y -valued Function-like total quasi_total Element of bool [:X,Y:]
vseq [;] (f,tseq) is Relation-like Function-like set
Funcs (X,Y) is non empty functional FUNCTION_DOMAIN of X,Y
dom tseq is set
(dom tseq) --> f is Relation-like dom tseq -defined {f} -valued Function-like constant total quasi_total V134() V135() V136() Element of bool [:(dom tseq),{f}:]
{f} is non empty V144() V145() V146() set
[:(dom tseq),{f}:] is V134() V135() V136() set
bool [:(dom tseq),{f}:] is non empty set
[:X,REAL:] is V134() V135() V136() set
bool [:X,REAL:] is non empty set
[:X,[:REAL,Y:]:] is set
bool [:X,[:REAL,Y:]:] is non empty set
<:((dom tseq) --> f),tseq:> is Relation-like Function-like set
tseq is Relation-like X -defined [:REAL,Y:] -valued Function-like total quasi_total Element of bool [:X,[:REAL,Y:]:]
vseq * tseq is Relation-like X -defined Y -valued Function-like total quasi_total Element of bool [:X,Y:]
X is non empty set
Y is non empty addLoopStr
the carrier of Y is non empty set
Funcs (X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of X, the carrier of Y
[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] is non empty set
[:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
vseq is non empty Relation-like [:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
f is non empty Relation-like [:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
tseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
tseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
vseq . (tseq,tseq) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[tseq,tseq] is set
vseq . [tseq,tseq] is Relation-like Function-like set
the addF of Y .: (tseq,tseq) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
f . (tseq,tseq) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
f . [tseq,tseq] is Relation-like Function-like set
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V104() RLSStruct
the carrier of Y is non empty set
Funcs (X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of X, the carrier of Y
[:REAL,(Funcs (X, the carrier of Y)):] is non empty set
[:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
vseq is non empty Relation-like [:REAL,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
f is ext-real V31() real Element of REAL
tseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[f,tseq] is Element of [:REAL,(Funcs (X, the carrier of Y)):]
vseq . [f,tseq] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
tseq is Element of X
(vseq . [f,tseq]) . tseq is Element of the carrier of Y
tseq . tseq is Element of the carrier of Y
f * (tseq . tseq) is Element of the carrier of Y
the Mult of Y . (f,(tseq . tseq)) is set
[f,(tseq . tseq)] is set
the Mult of Y . [f,(tseq . tseq)] is set
dom (vseq . [f,tseq]) is set
vseq . (f,tseq) is Relation-like Function-like Element of Funcs (X, the carrier of Y)
[f,tseq] is set
vseq . [f,tseq] is Relation-like Function-like set
(X, the carrier of Y, the Mult of Y,f,tseq) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
vseq is non empty Relation-like [:REAL,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
f is non empty Relation-like [:REAL,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
tseq is ext-real V31() real Element of REAL
tseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[tseq,tseq] is Element of [:REAL,(Funcs (X, the carrier of Y)):]
vseq . [tseq,tseq] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
tseq is Element of X
(vseq . [tseq,tseq]) . tseq is Element of the carrier of Y
tseq . tseq is Element of the carrier of Y
tseq * (tseq . tseq) is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
the Mult of Y . (tseq,(tseq . tseq)) is set
[tseq,(tseq . tseq)] is set
the Mult of Y . [tseq,(tseq . tseq)] is set
f . [tseq,tseq] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
(f . [tseq,tseq]) . tseq is Element of the carrier of Y
vseq . (tseq,tseq) is Relation-like Function-like Element of Funcs (X, the carrier of Y)
[tseq,tseq] is set
vseq . [tseq,tseq] is Relation-like Function-like set
f . (tseq,tseq) is Relation-like Function-like Element of Funcs (X, the carrier of Y)
f . [tseq,tseq] is Relation-like Function-like set
Y is non empty ZeroStr
the carrier of Y is non empty set
X is set
0. Y is V53(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
X --> (0. Y) is Relation-like X -defined the carrier of Y -valued Function-like constant total quasi_total Element of bool [:X, the carrier of Y:]
[:X, the carrier of Y:] is set
bool [:X, the carrier of Y:] is non empty set
Funcs (X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of X, the carrier of Y
X is non empty set
Y is non empty set
[:X,Y:] is non empty set
bool [:X,Y:] is non empty set
vseq is Element of X
f is non empty Relation-like X -defined Y -valued Function-like total quasi_total Element of bool [:X,Y:]
dom f is set
X is non empty set
Y is non empty addLoopStr
the carrier of Y is non empty set
Funcs (X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of X, the carrier of Y
(X,Y) is non empty Relation-like [:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] is non empty set
[:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
tseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
vseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
f is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
(X,Y) . (vseq,f) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[vseq,f] is set
(X,Y) . [vseq,f] is Relation-like Function-like set
tseq is Element of X
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the addF of Y .: (vseq,f) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
dom ( the addF of Y .: (vseq,f)) is set
tseq . tseq is Element of the carrier of Y
( the addF of Y .: (vseq,f)) . tseq is Element of the carrier of Y
vseq . tseq is Element of the carrier of Y
f . tseq is Element of the carrier of Y
(vseq . tseq) + (f . tseq) is Element of the carrier of Y
the addF of Y . ((vseq . tseq),(f . tseq)) is Element of the carrier of Y
[(vseq . tseq),(f . tseq)] is set
the addF of Y . [(vseq . tseq),(f . tseq)] is set
tseq is Element of X
((X,Y) . (vseq,f)) . tseq is Element of the carrier of Y
( the addF of Y .: (vseq,f)) . tseq is Element of the carrier of Y
vseq . tseq is Element of the carrier of Y
f . tseq is Element of the carrier of Y
(vseq . tseq) + (f . tseq) is Element of the carrier of Y
the addF of Y . ((vseq . tseq),(f . tseq)) is Element of the carrier of Y
[(vseq . tseq),(f . tseq)] is set
the addF of Y . [(vseq . tseq),(f . tseq)] is set
tseq . tseq is Element of the carrier of Y
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V104() RLSStruct
the carrier of Y is non empty set
Funcs (X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of X, the carrier of Y
(X,Y) is non empty Relation-like [:REAL,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:REAL,(Funcs (X, the carrier of Y)):] is non empty set
[:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
vseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
f is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
tseq is ext-real V31() real Element of REAL
[tseq,f] is Element of [:REAL,(Funcs (X, the carrier of Y)):]
(X,Y) . [tseq,f] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
tseq is Element of X
vseq . tseq is Element of the carrier of Y
f . tseq is Element of the carrier of Y
tseq * (f . tseq) is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
the Mult of Y . (tseq,(f . tseq)) is set
[tseq,(f . tseq)] is set
the Mult of Y . [tseq,(f . tseq)] is set
tseq is Element of X
vseq . tseq is Element of the carrier of Y
((X,Y) . [tseq,f]) . tseq is Element of the carrier of Y
f . tseq is Element of the carrier of Y
tseq * (f . tseq) is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
the Mult of Y . (tseq,(f . tseq)) is set
[tseq,(f . tseq)] is set
the Mult of Y . [tseq,(f . tseq)] is set
tseq is Element of X
vseq . tseq is Element of the carrier of Y
f . tseq is Element of the carrier of Y
tseq * (f . tseq) is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
the Mult of Y . (tseq,(f . tseq)) is set
[tseq,(f . tseq)] is set
the Mult of Y . [tseq,(f . tseq)] is set
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V104() RLSStruct
the carrier of Y is non empty set
Funcs (X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of X, the carrier of Y
(X,Y) is non empty Relation-like [:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] is non empty set
[:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
vseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
f is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
(X,Y) . (vseq,f) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[vseq,f] is set
(X,Y) . [vseq,f] is Relation-like Function-like set
(X,Y) . (f,vseq) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[f,vseq] is set
(X,Y) . [f,vseq] is Relation-like Function-like set
tseq is Element of X
((X,Y) . (vseq,f)) . tseq is Element of the carrier of Y
f . tseq is Element of the carrier of Y
vseq . tseq is Element of the carrier of Y
(f . tseq) + (vseq . tseq) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the addF of Y . ((f . tseq),(vseq . tseq)) is Element of the carrier of Y
[(f . tseq),(vseq . tseq)] is set
the addF of Y . [(f . tseq),(vseq . tseq)] is set
((X,Y) . (f,vseq)) . tseq is Element of the carrier of Y
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V104() RLSStruct
the carrier of Y is non empty set
Funcs (X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of X, the carrier of Y
(X,Y) is non empty Relation-like [:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] is non empty set
[:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
vseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
f is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
(X,Y) . (vseq,f) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[vseq,f] is set
(X,Y) . [vseq,f] is Relation-like Function-like set
tseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
(X,Y) . (f,tseq) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[f,tseq] is set
(X,Y) . [f,tseq] is Relation-like Function-like set
(X,Y) . (vseq,((X,Y) . (f,tseq))) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[vseq,((X,Y) . (f,tseq))] is set
(X,Y) . [vseq,((X,Y) . (f,tseq))] is Relation-like Function-like set
(X,Y) . (((X,Y) . (vseq,f)),tseq) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[((X,Y) . (vseq,f)),tseq] is set
(X,Y) . [((X,Y) . (vseq,f)),tseq] is Relation-like Function-like set
tseq is Element of X
((X,Y) . (vseq,((X,Y) . (f,tseq)))) . tseq is Element of the carrier of Y
vseq . tseq is Element of the carrier of Y
((X,Y) . (f,tseq)) . tseq is Element of the carrier of Y
(vseq . tseq) + (((X,Y) . (f,tseq)) . tseq) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the addF of Y . ((vseq . tseq),(((X,Y) . (f,tseq)) . tseq)) is Element of the carrier of Y
[(vseq . tseq),(((X,Y) . (f,tseq)) . tseq)] is set
the addF of Y . [(vseq . tseq),(((X,Y) . (f,tseq)) . tseq)] is set
f . tseq is Element of the carrier of Y
tseq . tseq is Element of the carrier of Y
(f . tseq) + (tseq . tseq) is Element of the carrier of Y
the addF of Y . ((f . tseq),(tseq . tseq)) is Element of the carrier of Y
[(f . tseq),(tseq . tseq)] is set
the addF of Y . [(f . tseq),(tseq . tseq)] is set
(vseq . tseq) + ((f . tseq) + (tseq . tseq)) is Element of the carrier of Y
the addF of Y . ((vseq . tseq),((f . tseq) + (tseq . tseq))) is Element of the carrier of Y
[(vseq . tseq),((f . tseq) + (tseq . tseq))] is set
the addF of Y . [(vseq . tseq),((f . tseq) + (tseq . tseq))] is set
(vseq . tseq) + (f . tseq) is Element of the carrier of Y
the addF of Y . ((vseq . tseq),(f . tseq)) is Element of the carrier of Y
[(vseq . tseq),(f . tseq)] is set
the addF of Y . [(vseq . tseq),(f . tseq)] is set
((vseq . tseq) + (f . tseq)) + (tseq . tseq) is Element of the carrier of Y
the addF of Y . (((vseq . tseq) + (f . tseq)),(tseq . tseq)) is Element of the carrier of Y
[((vseq . tseq) + (f . tseq)),(tseq . tseq)] is set
the addF of Y . [((vseq . tseq) + (f . tseq)),(tseq . tseq)] is set
((X,Y) . (vseq,f)) . tseq is Element of the carrier of Y
(((X,Y) . (vseq,f)) . tseq) + (tseq . tseq) is Element of the carrier of Y
the addF of Y . ((((X,Y) . (vseq,f)) . tseq),(tseq . tseq)) is Element of the carrier of Y
[(((X,Y) . (vseq,f)) . tseq),(tseq . tseq)] is set
the addF of Y . [(((X,Y) . (vseq,f)) . tseq),(tseq . tseq)] is set
((X,Y) . (((X,Y) . (vseq,f)),tseq)) . tseq is Element of the carrier of Y
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V104() RLSStruct
the carrier of Y is non empty set
Funcs (X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of X, the carrier of Y
(X,Y) is non empty Relation-like [:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] is non empty set
[:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
(X,Y) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
0. Y is V53(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
X --> (0. Y) is non empty Relation-like X -defined the carrier of Y -valued Function-like constant total quasi_total Element of bool [:X, the carrier of Y:]
[:X, the carrier of Y:] is non empty set
bool [:X, the carrier of Y:] is non empty set
vseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
(X,Y) . ((X,Y),vseq) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[(X,Y),vseq] is set
(X,Y) . [(X,Y),vseq] is Relation-like Function-like set
f is Element of X
((X,Y) . ((X,Y),vseq)) . f is Element of the carrier of Y
(X,Y) . f is Element of the carrier of Y
vseq . f is Element of the carrier of Y
((X,Y) . f) + (vseq . f) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the addF of Y . (((X,Y) . f),(vseq . f)) is Element of the carrier of Y
[((X,Y) . f),(vseq . f)] is set
the addF of Y . [((X,Y) . f),(vseq . f)] is set
(0. Y) + (vseq . f) is Element of the carrier of Y
the addF of Y . ((0. Y),(vseq . f)) is Element of the carrier of Y
[(0. Y),(vseq . f)] is set
the addF of Y . [(0. Y),(vseq . f)] is set
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V104() RLSStruct
the carrier of Y is non empty set
Funcs (X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of X, the carrier of Y
(X,Y) is non empty Relation-like [:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] is non empty set
[:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
(X,Y) is non empty Relation-like [:REAL,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:REAL,(Funcs (X, the carrier of Y)):] is non empty set
[:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
(X,Y) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
0. Y is V53(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
X --> (0. Y) is non empty Relation-like X -defined the carrier of Y -valued Function-like constant total quasi_total Element of bool [:X, the carrier of Y:]
[:X, the carrier of Y:] is non empty set
bool [:X, the carrier of Y:] is non empty set
vseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[(- 1),vseq] is Element of [:REAL,(Funcs (X, the carrier of Y)):]
(X,Y) . [(- 1),vseq] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
(X,Y) . (vseq,((X,Y) . [(- 1),vseq])) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[vseq,((X,Y) . [(- 1),vseq])] is set
(X,Y) . [vseq,((X,Y) . [(- 1),vseq])] is Relation-like Function-like set
f is Element of X
vseq . f is Element of the carrier of Y
((X,Y) . (vseq,((X,Y) . [(- 1),vseq]))) . f is Element of the carrier of Y
((X,Y) . [(- 1),vseq]) . f is Element of the carrier of Y
(vseq . f) + (((X,Y) . [(- 1),vseq]) . f) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the addF of Y . ((vseq . f),(((X,Y) . [(- 1),vseq]) . f)) is Element of the carrier of Y
[(vseq . f),(((X,Y) . [(- 1),vseq]) . f)] is set
the addF of Y . [(vseq . f),(((X,Y) . [(- 1),vseq]) . f)] is set
(- 1) * (vseq . f) is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
the Mult of Y . ((- 1),(vseq . f)) is set
[(- 1),(vseq . f)] is set
the Mult of Y . [(- 1),(vseq . f)] is set
(vseq . f) + ((- 1) * (vseq . f)) is Element of the carrier of Y
the addF of Y . ((vseq . f),((- 1) * (vseq . f))) is Element of the carrier of Y
[(vseq . f),((- 1) * (vseq . f))] is set
the addF of Y . [(vseq . f),((- 1) * (vseq . f))] is set
- (vseq . f) is Element of the carrier of Y
(vseq . f) + (- (vseq . f)) is Element of the carrier of Y
the addF of Y . ((vseq . f),(- (vseq . f))) is Element of the carrier of Y
[(vseq . f),(- (vseq . f))] is set
the addF of Y . [(vseq . f),(- (vseq . f))] is set
(X,Y) . f is Element of the carrier of Y
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V104() RLSStruct
the carrier of Y is non empty set
Funcs (X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of X, the carrier of Y
(X,Y) is non empty Relation-like [:REAL,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:REAL,(Funcs (X, the carrier of Y)):] is non empty set
[:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
vseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[1,vseq] is Element of [:NAT,(Funcs (X, the carrier of Y)):]
[:NAT,(Funcs (X, the carrier of Y)):] is non empty set
(X,Y) . [1,vseq] is Relation-like Function-like set
[1,vseq] is Element of [:REAL,(Funcs (X, the carrier of Y)):]
(X,Y) . [1,vseq] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
f is Element of X
((X,Y) . [1,vseq]) . f is Element of the carrier of Y
vseq . f is Element of the carrier of Y
1 * (vseq . f) is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
the Mult of Y . (1,(vseq . f)) is set
[1,(vseq . f)] is set
the Mult of Y . [1,(vseq . f)] is set
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V104() RLSStruct
the carrier of Y is non empty set
Funcs (X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of X, the carrier of Y
(X,Y) is non empty Relation-like [:REAL,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:REAL,(Funcs (X, the carrier of Y)):] is non empty set
[:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
vseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
f is ext-real V31() real Element of REAL
tseq is ext-real V31() real Element of REAL
[tseq,vseq] is Element of [:REAL,(Funcs (X, the carrier of Y)):]
(X,Y) . [tseq,vseq] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[f,((X,Y) . [tseq,vseq])] is Element of [:REAL,(Funcs (X, the carrier of Y)):]
(X,Y) . [f,((X,Y) . [tseq,vseq])] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
f * tseq is ext-real V31() real Element of REAL
[(f * tseq),vseq] is Element of [:REAL,(Funcs (X, the carrier of Y)):]
(X,Y) . [(f * tseq),vseq] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
tseq is Element of X
((X,Y) . [f,((X,Y) . [tseq,vseq])]) . tseq is Element of the carrier of Y
((X,Y) . [tseq,vseq]) . tseq is Element of the carrier of Y
f * (((X,Y) . [tseq,vseq]) . tseq) is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
the Mult of Y . (f,(((X,Y) . [tseq,vseq]) . tseq)) is set
[f,(((X,Y) . [tseq,vseq]) . tseq)] is set
the Mult of Y . [f,(((X,Y) . [tseq,vseq]) . tseq)] is set
vseq . tseq is Element of the carrier of Y
tseq * (vseq . tseq) is Element of the carrier of Y
the Mult of Y . (tseq,(vseq . tseq)) is set
[tseq,(vseq . tseq)] is set
the Mult of Y . [tseq,(vseq . tseq)] is set
f * (tseq * (vseq . tseq)) is Element of the carrier of Y
the Mult of Y . (f,(tseq * (vseq . tseq))) is set
[f,(tseq * (vseq . tseq))] is set
the Mult of Y . [f,(tseq * (vseq . tseq))] is set
(f * tseq) * (vseq . tseq) is Element of the carrier of Y
the Mult of Y . ((f * tseq),(vseq . tseq)) is set
[(f * tseq),(vseq . tseq)] is set
the Mult of Y . [(f * tseq),(vseq . tseq)] is set
((X,Y) . [(f * tseq),vseq]) . tseq is Element of the carrier of Y
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V104() RLSStruct
the carrier of Y is non empty set
Funcs (X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of X, the carrier of Y
(X,Y) is non empty Relation-like [:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] is non empty set
[:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
(X,Y) is non empty Relation-like [:REAL,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:REAL,(Funcs (X, the carrier of Y)):] is non empty set
[:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
vseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
f is ext-real V31() real Element of REAL
[f,vseq] is Element of [:REAL,(Funcs (X, the carrier of Y)):]
(X,Y) . [f,vseq] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
tseq is ext-real V31() real Element of REAL
[tseq,vseq] is Element of [:REAL,(Funcs (X, the carrier of Y)):]
(X,Y) . [tseq,vseq] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
(X,Y) . (((X,Y) . [f,vseq]),((X,Y) . [tseq,vseq])) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[((X,Y) . [f,vseq]),((X,Y) . [tseq,vseq])] is set
(X,Y) . [((X,Y) . [f,vseq]),((X,Y) . [tseq,vseq])] is Relation-like Function-like set
f + tseq is ext-real V31() real Element of REAL
[(f + tseq),vseq] is Element of [:REAL,(Funcs (X, the carrier of Y)):]
(X,Y) . [(f + tseq),vseq] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
tseq is Element of X
((X,Y) . (((X,Y) . [f,vseq]),((X,Y) . [tseq,vseq]))) . tseq is Element of the carrier of Y
((X,Y) . [f,vseq]) . tseq is Element of the carrier of Y
((X,Y) . [tseq,vseq]) . tseq is Element of the carrier of Y
(((X,Y) . [f,vseq]) . tseq) + (((X,Y) . [tseq,vseq]) . tseq) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the addF of Y . ((((X,Y) . [f,vseq]) . tseq),(((X,Y) . [tseq,vseq]) . tseq)) is Element of the carrier of Y
[(((X,Y) . [f,vseq]) . tseq),(((X,Y) . [tseq,vseq]) . tseq)] is set
the addF of Y . [(((X,Y) . [f,vseq]) . tseq),(((X,Y) . [tseq,vseq]) . tseq)] is set
vseq . tseq is Element of the carrier of Y
f * (vseq . tseq) is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
the Mult of Y . (f,(vseq . tseq)) is set
[f,(vseq . tseq)] is set
the Mult of Y . [f,(vseq . tseq)] is set
(f * (vseq . tseq)) + (((X,Y) . [tseq,vseq]) . tseq) is Element of the carrier of Y
the addF of Y . ((f * (vseq . tseq)),(((X,Y) . [tseq,vseq]) . tseq)) is Element of the carrier of Y
[(f * (vseq . tseq)),(((X,Y) . [tseq,vseq]) . tseq)] is set
the addF of Y . [(f * (vseq . tseq)),(((X,Y) . [tseq,vseq]) . tseq)] is set
tseq * (vseq . tseq) is Element of the carrier of Y
the Mult of Y . (tseq,(vseq . tseq)) is set
[tseq,(vseq . tseq)] is set
the Mult of Y . [tseq,(vseq . tseq)] is set
(f * (vseq . tseq)) + (tseq * (vseq . tseq)) is Element of the carrier of Y
the addF of Y . ((f * (vseq . tseq)),(tseq * (vseq . tseq))) is Element of the carrier of Y
[(f * (vseq . tseq)),(tseq * (vseq . tseq))] is set
the addF of Y . [(f * (vseq . tseq)),(tseq * (vseq . tseq))] is set
(f + tseq) * (vseq . tseq) is Element of the carrier of Y
the Mult of Y . ((f + tseq),(vseq . tseq)) is set
[(f + tseq),(vseq . tseq)] is set
the Mult of Y . [(f + tseq),(vseq . tseq)] is set
((X,Y) . [(f + tseq),vseq]) . tseq is Element of the carrier of Y
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V104() RLSStruct
the carrier of Y is non empty set
Funcs (X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of X, the carrier of Y
(X,Y) is non empty Relation-like [:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] is non empty set
[:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
(X,Y) is non empty Relation-like [:REAL,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:REAL,(Funcs (X, the carrier of Y)):] is non empty set
[:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
vseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
f is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
(X,Y) . (vseq,f) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[vseq,f] is set
(X,Y) . [vseq,f] is Relation-like Function-like set
tseq is ext-real V31() real Element of REAL
[tseq,vseq] is Element of [:REAL,(Funcs (X, the carrier of Y)):]
(X,Y) . [tseq,vseq] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[tseq,f] is Element of [:REAL,(Funcs (X, the carrier of Y)):]
(X,Y) . [tseq,f] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
(X,Y) . (((X,Y) . [tseq,vseq]),((X,Y) . [tseq,f])) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[((X,Y) . [tseq,vseq]),((X,Y) . [tseq,f])] is set
(X,Y) . [((X,Y) . [tseq,vseq]),((X,Y) . [tseq,f])] is Relation-like Function-like set
[tseq,((X,Y) . (vseq,f))] is Element of [:REAL,(Funcs (X, the carrier of Y)):]
(X,Y) . [tseq,((X,Y) . (vseq,f))] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
tseq is Element of X
((X,Y) . (((X,Y) . [tseq,vseq]),((X,Y) . [tseq,f]))) . tseq is Element of the carrier of Y
((X,Y) . [tseq,vseq]) . tseq is Element of the carrier of Y
((X,Y) . [tseq,f]) . tseq is Element of the carrier of Y
(((X,Y) . [tseq,vseq]) . tseq) + (((X,Y) . [tseq,f]) . tseq) is Element of the carrier of Y
the addF of Y is non empty Relation-like [: the carrier of Y, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:]
[: the carrier of Y, the carrier of Y:] is non empty set
[:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[: the carrier of Y, the carrier of Y:], the carrier of Y:] is non empty set
the addF of Y . ((((X,Y) . [tseq,vseq]) . tseq),(((X,Y) . [tseq,f]) . tseq)) is Element of the carrier of Y
[(((X,Y) . [tseq,vseq]) . tseq),(((X,Y) . [tseq,f]) . tseq)] is set
the addF of Y . [(((X,Y) . [tseq,vseq]) . tseq),(((X,Y) . [tseq,f]) . tseq)] is set
vseq . tseq is Element of the carrier of Y
tseq * (vseq . tseq) is Element of the carrier of Y
the Mult of Y is non empty Relation-like [:REAL, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of Y:], the carrier of Y:]
[:REAL, the carrier of Y:] is non empty set
[:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[:REAL, the carrier of Y:], the carrier of Y:] is non empty set
the Mult of Y . (tseq,(vseq . tseq)) is set
[tseq,(vseq . tseq)] is set
the Mult of Y . [tseq,(vseq . tseq)] is set
(tseq * (vseq . tseq)) + (((X,Y) . [tseq,f]) . tseq) is Element of the carrier of Y
the addF of Y . ((tseq * (vseq . tseq)),(((X,Y) . [tseq,f]) . tseq)) is Element of the carrier of Y
[(tseq * (vseq . tseq)),(((X,Y) . [tseq,f]) . tseq)] is set
the addF of Y . [(tseq * (vseq . tseq)),(((X,Y) . [tseq,f]) . tseq)] is set
f . tseq is Element of the carrier of Y
tseq * (f . tseq) is Element of the carrier of Y
the Mult of Y . (tseq,(f . tseq)) is set
[tseq,(f . tseq)] is set
the Mult of Y . [tseq,(f . tseq)] is set
(tseq * (vseq . tseq)) + (tseq * (f . tseq)) is Element of the carrier of Y
the addF of Y . ((tseq * (vseq . tseq)),(tseq * (f . tseq))) is Element of the carrier of Y
[(tseq * (vseq . tseq)),(tseq * (f . tseq))] is set
the addF of Y . [(tseq * (vseq . tseq)),(tseq * (f . tseq))] is set
(vseq . tseq) + (f . tseq) is Element of the carrier of Y
the addF of Y . ((vseq . tseq),(f . tseq)) is Element of the carrier of Y
[(vseq . tseq),(f . tseq)] is set
the addF of Y . [(vseq . tseq),(f . tseq)] is set
tseq * ((vseq . tseq) + (f . tseq)) is Element of the carrier of Y
the Mult of Y . (tseq,((vseq . tseq) + (f . tseq))) is set
[tseq,((vseq . tseq) + (f . tseq))] is set
the Mult of Y . [tseq,((vseq . tseq) + (f . tseq))] is set
((X,Y) . (vseq,f)) . tseq is Element of the carrier of Y
tseq * (((X,Y) . (vseq,f)) . tseq) is Element of the carrier of Y
the Mult of Y . (tseq,(((X,Y) . (vseq,f)) . tseq)) is set
[tseq,(((X,Y) . (vseq,f)) . tseq)] is set
the Mult of Y . [tseq,(((X,Y) . (vseq,f)) . tseq)] is set
((X,Y) . [tseq,((X,Y) . (vseq,f))]) . tseq is Element of the carrier of Y
X is non empty set
Y is non empty left_complementable right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital V104() RLSStruct
the carrier of Y is non empty set
Funcs (X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of X, the carrier of Y
(X,Y) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
0. Y is V53(Y) Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
X --> (0. Y) is non empty Relation-like X -defined the carrier of Y -valued Function-like constant total quasi_total Element of bool [:X, the carrier of Y:]
[:X, the carrier of Y:] is non empty set
bool [:X, the carrier of Y:] is non empty set
(X,Y) is non empty Relation-like [:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):] is non empty set
[:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:(Funcs (X, the carrier of Y)),(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
(X,Y) is non empty Relation-like [:REAL,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V110() Element of bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:REAL,(Funcs (X, the carrier of Y)):] is non empty set
[:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:REAL,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) is non empty strict RLSStruct
the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) is non empty set
vseq is ext-real V31() real set
f is ext-real V31() real set
vseq * f is ext-real V31() real set
tseq is ext-real V31() real Element of REAL
tseq is ext-real V31() real Element of REAL
tseq * tseq is ext-real V31() real Element of REAL
tseq is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
(tseq * tseq) * tseq is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) is non empty Relation-like [:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] -defined the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):], the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):]
[:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] is non empty set
[:[:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):], the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] is non empty set
bool [:[:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):], the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] is non empty set
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . ((tseq * tseq),tseq) is set
[(tseq * tseq),tseq] is set
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . [(tseq * tseq),tseq] is set
tseq * tseq is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . (tseq,tseq) is set
[tseq,tseq] is set
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . [tseq,tseq] is set
tseq * (tseq * tseq) is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . (tseq,(tseq * tseq)) is set
[tseq,(tseq * tseq)] is set
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . [tseq,(tseq * tseq)] is set
tseq is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
(vseq * f) * tseq is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) is non empty Relation-like [:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] -defined the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):], the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):]
[:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] is non empty set
[:[:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):], the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] is non empty set
bool [:[:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):], the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] is non empty set
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . ((vseq * f),tseq) is set
[(vseq * f),tseq] is set
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . [(vseq * f),tseq] is set
f * tseq is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . (f,tseq) is set
[f,tseq] is set
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . [f,tseq] is set
vseq * (f * tseq) is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . (vseq,(f * tseq)) is set
[vseq,(f * tseq)] is set
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . [vseq,(f * tseq)] is set
vseq is ext-real V31() real set
f is ext-real V31() real set
vseq + f is ext-real V31() real set
tseq is ext-real V31() real Element of REAL
tseq is ext-real V31() real Element of REAL
tseq + tseq is ext-real V31() real Element of REAL
tseq is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
(tseq + tseq) * tseq is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) is non empty Relation-like [:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] -defined the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):], the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):]
[:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] is non empty set
[:[:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):], the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] is non empty set
bool [:[:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):], the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] is non empty set
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . ((tseq + tseq),tseq) is set
[(tseq + tseq),tseq] is set
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . [(tseq + tseq),tseq] is set
tseq * tseq is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . (tseq,tseq) is set
[tseq,tseq] is set
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . [tseq,tseq] is set
tseq * tseq is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . (tseq,tseq) is set
[tseq,tseq] is set
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . [tseq,tseq] is set
(tseq * tseq) + (tseq * tseq) is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
the addF of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) is non empty Relation-like [: the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #), the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] -defined the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) -valued Function-like total quasi_total Element of bool [:[: the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #), the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):], the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):]
[: the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #), the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] is non empty set
[:[: the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #), the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):], the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] is non empty set
bool [:[: the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #), the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):], the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] is non empty set
the addF of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . ((tseq * tseq),(tseq * tseq)) is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
[(tseq * tseq),(tseq * tseq)] is set
the addF of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . [(tseq * tseq),(tseq * tseq)] is set
tseq is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
(vseq + f) * tseq is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) is non empty Relation-like [:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] -defined the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) -valued Function-like total quasi_total Element of bool [:[:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):], the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):]
[:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] is non empty set
[:[:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):], the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] is non empty set
bool [:[:REAL, the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):], the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #):] is non empty set
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . ((vseq + f),tseq) is set
[(vseq + f),tseq] is set
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . [(vseq + f),tseq] is set
vseq * tseq is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . (vseq,tseq) is set
[vseq,tseq] is set
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . [vseq,tseq] is set
f * tseq is Element of the carrier of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #)
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . (f,tseq) is set
[f,tseq] is set
the Mult of RLSStruct(# (Funcs (X, the carrier of Y)),(X,Y),(X,Y),(X,Y) #) . [f,tseq] is set
(vseq * tseq) + (f * tseq) is Element of the carrier of RLSStruct(# (