:: LOPBAN_1 semantic presentation

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