REAL is non empty V35() V142() V143() V144() V148() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V142() V143() V144() V145() V146() V147() V148() Element of bool REAL
bool REAL is non empty set
COMPLEX is non empty V35() V142() V148() set
omega is non empty epsilon-transitive epsilon-connected ordinal V142() V143() V144() V145() V146() V147() V148() set
bool omega is non empty set
bool NAT is non empty set
RAT is non empty V35() V142() V143() V144() V145() V148() set
INT is non empty V35() V142() V143() V144() V145() V146() V148() set
[:REAL,REAL:] is non empty V132() V133() V134() set
bool [:REAL,REAL:] is non empty set
K373() is non empty strict multMagma
the carrier of K373() is non empty set
<REAL,+> is non empty strict V110() V111() V112() V114() left-invertible right-invertible invertible left-cancelable right-cancelable V169() multMagma
K379() is non empty strict V112() V114() left-cancelable right-cancelable V169() SubStr of <REAL,+>
<NAT,+> is non empty strict V110() V112() V114() left-cancelable right-cancelable V169() uniquely-decomposable SubStr of K379()
<REAL,*> is non empty strict V110() V112() V114() multMagma
<NAT,*> is non empty strict V110() V112() V114() uniquely-decomposable SubStr of <REAL,*>
[:NAT,REAL:] is non empty V132() V133() V134() set
bool [:NAT,REAL:] is non empty set
[:NAT,COMPLEX:] is non empty V132() set
bool [:NAT,COMPLEX:] is non empty set
K428() is non empty set
[:K428(),K428():] is non empty set
[:[:K428(),K428():],K428():] is non empty set
bool [:[:K428(),K428():],K428():] is non empty set
[:COMPLEX,K428():] is non empty set
[:[:COMPLEX,K428():],K428():] is non empty set
bool [:[:COMPLEX,K428():],K428():] is non empty set
K434() is non empty strict CLSStruct
the carrier of K434() is non empty set
bool the carrier of K434() is non empty set
K438() is Element of bool the carrier of K434()
[:K438(),K438():] is set
[:[:K438(),K438():],COMPLEX:] is V132() set
bool [:[:K438(),K438():],COMPLEX:] is non empty set
the_set_of_l1ComplexSequences is non empty linearly-closed Element of bool the carrier of K434()
[:the_set_of_l1ComplexSequences,REAL:] is non empty V132() V133() V134() set
bool [:the_set_of_l1ComplexSequences,REAL:] is non empty set
[:COMPLEX,COMPLEX:] is non empty V132() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:COMPLEX,REAL:] is non empty V132() V133() V134() set
bool [:COMPLEX,REAL:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V132() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty V132() V133() V134() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is non empty RAT -valued V132() V133() V134() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty RAT -valued V132() V133() V134() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty RAT -valued INT -valued V132() V133() V134() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty RAT -valued INT -valued V132() V133() V134() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is non empty RAT -valued INT -valued V132() V133() V134() V135() set
[:[:NAT,NAT:],NAT:] is non empty RAT -valued INT -valued V132() V133() V134() V135() set
bool [:[:NAT,NAT:],NAT:] is non empty set
{} is empty Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real ext-real non positive non negative V142() V143() V144() V145() V146() V147() V148() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural complex real V108() V109() ext-real positive non negative V142() V143() V144() V145() V146() V147() Element of NAT
{{},1} is non empty V142() V143() V144() V145() V146() V147() set
0 is empty Function-like functional epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex real V108() V109() ext-real non positive non negative V142() V143() V144() V145() V146() V147() V148() Element of NAT
1r is complex Element of COMPLEX
- 1r is complex Element of COMPLEX
|.0.| is complex real V109() ext-real Element of REAL
Complex_l1_Space is non empty right_complementable Abelian add-associative right_zeroed discerning reflexive vector-distributive scalar-distributive scalar-associative scalar-unital ComplexNormSpace-like CNORMSTR
the carrier of Complex_l1_Space is non empty set
[:NAT, the carrier of Complex_l1_Space:] is non empty set
bool [:NAT, the carrier of Complex_l1_Space:] is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural complex real V108() V109() ext-real positive non negative V142() V143() V144() V145() V146() V147() Element of NAT
Y is non empty set
[:COMPLEX,Y:] is non empty set
[:[:COMPLEX,Y:],Y:] is non empty set
bool [:[:COMPLEX,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 [:COMPLEX,Y:] -defined Y -valued Function-like total quasi_total Element of bool [:[:COMPLEX,Y:],Y:]
f is complex 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 V132() Element of bool [:(dom tseq),{f}:]
{f} is non empty V142() set
[:(dom tseq),{f}:] is V132() set
bool [:(dom tseq),{f}:] is non empty set
[:X,COMPLEX:] is V132() set
bool [:X,COMPLEX:] is non empty set
[:X,[:COMPLEX,Y:]:] is set
bool [:X,[:COMPLEX,Y:]:] is non empty set
<:((dom tseq) --> f),tseq:> is Relation-like Function-like set
tseq is Relation-like X -defined [:COMPLEX,Y:] -valued Function-like total quasi_total Element of bool [:X,[:COMPLEX,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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
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
[:COMPLEX,(Funcs (X, the carrier of Y)):] is non empty set
[:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:COMPLEX,(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 [:COMPLEX, the carrier of Y:] -defined the carrier of Y -valued Function-like total quasi_total Element of bool [:[:COMPLEX, the carrier of Y:], the carrier of Y:]
[:COMPLEX, the carrier of Y:] is non empty set
[:[:COMPLEX, the carrier of Y:], the carrier of Y:] is non empty set
bool [:[:COMPLEX, the carrier of Y:], the carrier of Y:] is non empty set
vseq is non empty Relation-like [:COMPLEX,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V34() Element of bool [:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
f is complex 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)
[f,tseq] is set
vseq . [f,tseq] is Relation-like Function-like set
tseq is Element of X
(vseq . [f,tseq]) . tseq is set
tseq . tseq is Element of the carrier of Y
f * (tseq . tseq) is Element of the carrier of Y
tseq is complex Element of COMPLEX
[tseq,tseq] is Element of [:COMPLEX,(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)
dom (vseq . [tseq,tseq]) is set
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
(X, the carrier of Y, the Mult 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)
the Mult of Y . (f,(tseq . tseq)) is set
[f,(tseq . tseq)] is set
the Mult of Y . [f,(tseq . tseq)] is set
vseq is non empty Relation-like [:COMPLEX,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V34() Element of bool [:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
f is non empty Relation-like [:COMPLEX,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V34() Element of bool [:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
tseq is complex Element of COMPLEX
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 [:COMPLEX,(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
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
X is non empty set
Y is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
the carrier of Y is non empty set
FuncZero (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)
Funcs (X, the carrier of Y) is non empty functional FUNCTION_DOMAIN of X, the carrier of Y
0. Y is zero Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
vseq is Element of X
(FuncZero (X,Y)) . vseq 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 --> (0. Y)) . vseq is Element of the carrier of Y
X is non empty set
Y is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
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 [:COMPLEX,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V34() Element of bool [:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:COMPLEX,(Funcs (X, the carrier of Y)):] is non empty set
[:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:COMPLEX,(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 complex set
[tseq,f] is set
(X,Y) . [tseq,f] is Relation-like Function-like 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
tseq is complex Element of COMPLEX
[tseq,f] is Element of [:COMPLEX,(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
((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
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
X is non empty set
Y is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
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
FuncAdd (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 V34() 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)
(FuncAdd (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
(FuncAdd (X,Y)) . [vseq,f] is Relation-like Function-like set
(FuncAdd (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
(FuncAdd (X,Y)) . [f,vseq] is Relation-like Function-like set
tseq is Element of X
((FuncAdd (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
((FuncAdd (X,Y)) . (f,vseq)) . tseq is Element of the carrier of Y
X is non empty set
Y is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
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
FuncAdd (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 V34() 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)
(FuncAdd (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
(FuncAdd (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)
(FuncAdd (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
(FuncAdd (X,Y)) . [f,tseq] is Relation-like Function-like set
(FuncAdd (X,Y)) . (vseq,((FuncAdd (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,((FuncAdd (X,Y)) . (f,tseq))] is set
(FuncAdd (X,Y)) . [vseq,((FuncAdd (X,Y)) . (f,tseq))] is Relation-like Function-like set
(FuncAdd (X,Y)) . (((FuncAdd (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)
[((FuncAdd (X,Y)) . (vseq,f)),tseq] is set
(FuncAdd (X,Y)) . [((FuncAdd (X,Y)) . (vseq,f)),tseq] is Relation-like Function-like set
tseq is Element of X
((FuncAdd (X,Y)) . (vseq,((FuncAdd (X,Y)) . (f,tseq)))) . tseq is Element of the carrier of Y
vseq . tseq is Element of the carrier of Y
((FuncAdd (X,Y)) . (f,tseq)) . tseq is Element of the carrier of Y
(vseq . tseq) + (((FuncAdd (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),(((FuncAdd (X,Y)) . (f,tseq)) . tseq)) is Element of the carrier of Y
[(vseq . tseq),(((FuncAdd (X,Y)) . (f,tseq)) . tseq)] is set
the addF of Y . [(vseq . tseq),(((FuncAdd (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
((FuncAdd (X,Y)) . (vseq,f)) . tseq is Element of the carrier of Y
(((FuncAdd (X,Y)) . (vseq,f)) . tseq) + (tseq . tseq) is Element of the carrier of Y
the addF of Y . ((((FuncAdd (X,Y)) . (vseq,f)) . tseq),(tseq . tseq)) is Element of the carrier of Y
[(((FuncAdd (X,Y)) . (vseq,f)) . tseq),(tseq . tseq)] is set
the addF of Y . [(((FuncAdd (X,Y)) . (vseq,f)) . tseq),(tseq . tseq)] is set
((FuncAdd (X,Y)) . (((FuncAdd (X,Y)) . (vseq,f)),tseq)) . tseq is Element of the carrier of Y
X is non empty set
Y is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
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
FuncAdd (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 V34() 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
FuncZero (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)
vseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
(FuncAdd (X,Y)) . ((FuncZero (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)
[(FuncZero (X,Y)),vseq] is set
(FuncAdd (X,Y)) . [(FuncZero (X,Y)),vseq] is Relation-like Function-like set
f is Element of X
((FuncAdd (X,Y)) . ((FuncZero (X,Y)),vseq)) . f is Element of the carrier of Y
(FuncZero (X,Y)) . f is Element of the carrier of Y
vseq . f is Element of the carrier of Y
((FuncZero (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 . (((FuncZero (X,Y)) . f),(vseq . f)) is Element of the carrier of Y
[((FuncZero (X,Y)) . f),(vseq . f)] is set
the addF of Y . [((FuncZero (X,Y)) . f),(vseq . f)] is set
0. Y is zero Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
(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 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
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
FuncAdd (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 V34() 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 [:COMPLEX,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V34() Element of bool [:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:COMPLEX,(Funcs (X, the carrier of Y)):] is non empty set
[:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
FuncZero (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)
vseq is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[(- 1r),vseq] is Element of [:COMPLEX,(Funcs (X, the carrier of Y)):]
(X,Y) . [(- 1r),vseq] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
(FuncAdd (X,Y)) . (vseq,((X,Y) . [(- 1r),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) . [(- 1r),vseq])] is set
(FuncAdd (X,Y)) . [vseq,((X,Y) . [(- 1r),vseq])] is Relation-like Function-like set
f is Element of X
vseq . f is Element of the carrier of Y
((FuncAdd (X,Y)) . (vseq,((X,Y) . [(- 1r),vseq]))) . f is Element of the carrier of Y
((X,Y) . [(- 1r),vseq]) . f is Element of the carrier of Y
(vseq . f) + (((X,Y) . [(- 1r),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) . [(- 1r),vseq]) . f)) is Element of the carrier of Y
[(vseq . f),(((X,Y) . [(- 1r),vseq]) . f)] is set
the addF of Y . [(vseq . f),(((X,Y) . [(- 1r),vseq]) . f)] is set
(- 1r) * (vseq . f) is Element of the carrier of Y
(vseq . f) + ((- 1r) * (vseq . f)) is Element of the carrier of Y
the addF of Y . ((vseq . f),((- 1r) * (vseq . f))) is Element of the carrier of Y
[(vseq . f),((- 1r) * (vseq . f))] is set
the addF of Y . [(vseq . f),((- 1r) * (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
0. Y is zero Element of the carrier of Y
the ZeroF of Y is Element of the carrier of Y
(FuncZero (X,Y)) . f is Element of the carrier of Y
X is non empty set
Y is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
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 [:COMPLEX,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V34() Element of bool [:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:COMPLEX,(Funcs (X, the carrier of Y)):] is non empty set
[:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:COMPLEX,(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)
[1r,vseq] is Element of [:COMPLEX,(Funcs (X, the carrier of Y)):]
(X,Y) . [1r,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) . [1r,vseq]) . f is Element of the carrier of Y
vseq . f is Element of the carrier of Y
1r * (vseq . f) is Element of the carrier of Y
X is non empty set
Y is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
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 [:COMPLEX,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V34() Element of bool [:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:COMPLEX,(Funcs (X, the carrier of Y)):] is non empty set
[:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:COMPLEX,(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 complex set
tseq is complex set
[tseq,vseq] is set
(X,Y) . [tseq,vseq] is Relation-like Function-like set
[f,((X,Y) . [tseq,vseq])] is set
(X,Y) . [f,((X,Y) . [tseq,vseq])] is Relation-like Function-like set
f * tseq is complex set
[(f * tseq),vseq] is set
(X,Y) . [(f * tseq),vseq] is Relation-like Function-like set
tseq is complex Element of COMPLEX
tseq is complex Element of COMPLEX
[tseq,vseq] is Element of [:COMPLEX,(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,((X,Y) . [tseq,vseq])] is Element of [:COMPLEX,(Funcs (X, the carrier of Y)):]
(X,Y) . [tseq,((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)
tv is Element of X
((X,Y) . [tseq,((X,Y) . [tseq,vseq])]) . tv is Element of the carrier of Y
((X,Y) . [tseq,vseq]) . tv is Element of the carrier of Y
tseq * (((X,Y) . [tseq,vseq]) . tv) is Element of the carrier of Y
vseq . tv is Element of the carrier of Y
tseq * (vseq . tv) is Element of the carrier of Y
f * (tseq * (vseq . tv)) is Element of the carrier of Y
(f * tseq) * (vseq . tv) is Element of the carrier of Y
tseq * tseq is complex Element of COMPLEX
[(tseq * tseq),vseq] is Element of [:COMPLEX,(Funcs (X, the carrier of Y)):]
(X,Y) . [(tseq * 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) . [(tseq * tseq),vseq]) . tv is Element of the carrier of Y
X is non empty set
Y is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
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
FuncAdd (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 V34() 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 [:COMPLEX,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V34() Element of bool [:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:COMPLEX,(Funcs (X, the carrier of Y)):] is non empty set
[:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:COMPLEX,(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 complex set
[f,vseq] is set
(X,Y) . [f,vseq] is Relation-like Function-like set
tseq is complex set
[tseq,vseq] is set
(X,Y) . [tseq,vseq] is Relation-like Function-like set
(FuncAdd (X,Y)) . (((X,Y) . [f,vseq]),((X,Y) . [tseq,vseq])) is set
[((X,Y) . [f,vseq]),((X,Y) . [tseq,vseq])] is set
(FuncAdd (X,Y)) . [((X,Y) . [f,vseq]),((X,Y) . [tseq,vseq])] is Relation-like Function-like set
f + tseq is complex set
[(f + tseq),vseq] is set
(X,Y) . [(f + tseq),vseq] is Relation-like Function-like set
tseq is complex Element of COMPLEX
[tseq,vseq] is Element of [:COMPLEX,(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 is complex Element of COMPLEX
[tseq,vseq] is Element of [:COMPLEX,(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)
(FuncAdd (X,Y)) . (((X,Y) . [tseq,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) . [tseq,vseq]),((X,Y) . [tseq,vseq])] is set
(FuncAdd (X,Y)) . [((X,Y) . [tseq,vseq]),((X,Y) . [tseq,vseq])] is Relation-like Function-like set
tv is Element of X
((FuncAdd (X,Y)) . (((X,Y) . [tseq,vseq]),((X,Y) . [tseq,vseq]))) . tv is Element of the carrier of Y
((X,Y) . [tseq,vseq]) . tv is Element of the carrier of Y
((X,Y) . [tseq,vseq]) . tv is Element of the carrier of Y
(((X,Y) . [tseq,vseq]) . tv) + (((X,Y) . [tseq,vseq]) . tv) 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]) . tv),(((X,Y) . [tseq,vseq]) . tv)) is Element of the carrier of Y
[(((X,Y) . [tseq,vseq]) . tv),(((X,Y) . [tseq,vseq]) . tv)] is set
the addF of Y . [(((X,Y) . [tseq,vseq]) . tv),(((X,Y) . [tseq,vseq]) . tv)] is set
vseq . tv is Element of the carrier of Y
tseq * (vseq . tv) is Element of the carrier of Y
(tseq * (vseq . tv)) + (((X,Y) . [tseq,vseq]) . tv) is Element of the carrier of Y
the addF of Y . ((tseq * (vseq . tv)),(((X,Y) . [tseq,vseq]) . tv)) is Element of the carrier of Y
[(tseq * (vseq . tv)),(((X,Y) . [tseq,vseq]) . tv)] is set
the addF of Y . [(tseq * (vseq . tv)),(((X,Y) . [tseq,vseq]) . tv)] is set
f * (vseq . tv) is Element of the carrier of Y
tseq * (vseq . tv) is Element of the carrier of Y
(f * (vseq . tv)) + (tseq * (vseq . tv)) is Element of the carrier of Y
the addF of Y . ((f * (vseq . tv)),(tseq * (vseq . tv))) is Element of the carrier of Y
[(f * (vseq . tv)),(tseq * (vseq . tv))] is set
the addF of Y . [(f * (vseq . tv)),(tseq * (vseq . tv))] is set
(f + tseq) * (vseq . tv) is Element of the carrier of Y
tseq + tseq is complex Element of COMPLEX
[(tseq + tseq),vseq] is Element of [:COMPLEX,(Funcs (X, the carrier of Y)):]
(X,Y) . [(tseq + 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) . [(tseq + tseq),vseq]) . tv is Element of the carrier of Y
X is non empty set
Y is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
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
FuncAdd (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 V34() 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 [:COMPLEX,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V34() Element of bool [:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:COMPLEX,(Funcs (X, the carrier of Y)):] is non empty set
[:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:COMPLEX,(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)
(FuncAdd (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
(FuncAdd (X,Y)) . [vseq,f] is Relation-like Function-like set
tseq is complex set
[tseq,vseq] is set
(X,Y) . [tseq,vseq] is Relation-like Function-like set
[tseq,f] is set
(X,Y) . [tseq,f] is Relation-like Function-like set
(FuncAdd (X,Y)) . (((X,Y) . [tseq,vseq]),((X,Y) . [tseq,f])) is set
[((X,Y) . [tseq,vseq]),((X,Y) . [tseq,f])] is set
(FuncAdd (X,Y)) . [((X,Y) . [tseq,vseq]),((X,Y) . [tseq,f])] is Relation-like Function-like set
[tseq,((FuncAdd (X,Y)) . (vseq,f))] is set
(X,Y) . [tseq,((FuncAdd (X,Y)) . (vseq,f))] is Relation-like Function-like set
tseq is complex Element of COMPLEX
[tseq,vseq] is Element of [:COMPLEX,(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 [:COMPLEX,(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)
(FuncAdd (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
(FuncAdd (X,Y)) . [((X,Y) . [tseq,vseq]),((X,Y) . [tseq,f])] is Relation-like Function-like set
tseq is Element of X
((FuncAdd (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
(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
tseq * (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
(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
((FuncAdd (X,Y)) . (vseq,f)) . tseq is Element of the carrier of Y
tseq * (((FuncAdd (X,Y)) . (vseq,f)) . tseq) is Element of the carrier of Y
[tseq,((FuncAdd (X,Y)) . (vseq,f))] is Element of [:COMPLEX,(Funcs (X, the carrier of Y)):]
(X,Y) . [tseq,((FuncAdd (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)
((X,Y) . [tseq,((FuncAdd (X,Y)) . (vseq,f))]) . tseq is Element of the carrier of Y
X is non empty set
Y is non empty right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital CLSStruct
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
FuncZero (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)
FuncAdd (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 V34() 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 [:COMPLEX,(Funcs (X, the carrier of Y)):] -defined Funcs (X, the carrier of Y) -valued Function-like total quasi_total Function-yielding V34() Element of bool [:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):]
[:COMPLEX,(Funcs (X, the carrier of Y)):] is non empty set
[:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
bool [:[:COMPLEX,(Funcs (X, the carrier of Y)):],(Funcs (X, the carrier of Y)):] is non empty set
CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) is non empty strict CLSStruct
the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) is non empty set
f is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
f + tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) is non empty Relation-like [: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):] -defined the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) -valued Function-like total quasi_total Element of bool [:[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):], the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):]
[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):] is non empty set
[:[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):], the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):] is non empty set
bool [:[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):], the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):] is non empty set
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . (f,tseq) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
[f,tseq] is set
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . [f,tseq] is set
tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
(f + tseq) + tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . ((f + tseq),tseq) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
[(f + tseq),tseq] is set
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . [(f + tseq),tseq] is set
tseq + tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . (tseq,tseq) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
[tseq,tseq] is set
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . [tseq,tseq] is set
f + (tseq + tseq) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . (f,(tseq + tseq)) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
[f,(tseq + tseq)] is set
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . [f,(tseq + tseq)] is set
f is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,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)
[(- 1r),tseq] is Element of [:COMPLEX,(Funcs (X, the carrier of Y)):]
(X,Y) . [(- 1r),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 the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
f + tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) is non empty Relation-like [: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):] -defined the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) -valued Function-like total quasi_total Element of bool [:[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):], the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):]
[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):] is non empty set
[:[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):], the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):] is non empty set
bool [:[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):], the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):] is non empty set
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . (f,tseq) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
[f,tseq] is set
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . [f,tseq] is set
0. CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) is zero Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
the ZeroF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
f is complex set
tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
tseq + tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) is non empty Relation-like [: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):] -defined the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) -valued Function-like total quasi_total Element of bool [:[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):], the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):]
[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):] is non empty set
[:[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):], the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):] is non empty set
bool [:[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):], the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):] is non empty set
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . (tseq,tseq) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
[tseq,tseq] is set
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . [tseq,tseq] is set
f * (tseq + tseq) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
f * tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
f * tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
(f * tseq) + (f * tseq) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . ((f * tseq),(f * tseq)) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
[(f * tseq),(f * tseq)] is set
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . [(f * tseq),(f * tseq)] is set
tseq is complex Element of COMPLEX
tseq * (tseq + tseq) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
tseq * tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
tseq * tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
(tseq * tseq) + (tseq * tseq) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . ((tseq * tseq),(tseq * tseq)) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
[(tseq * tseq),(tseq * tseq)] is set
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . [(tseq * tseq),(tseq * tseq)] is set
e is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[tseq,e] is Element of [:COMPLEX,(Funcs (X, the carrier of Y)):]
(X,Y) . [tseq,e] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
tv is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[tseq,tv] is Element of [:COMPLEX,(Funcs (X, the carrier of Y)):]
(X,Y) . [tseq,tv] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
(FuncAdd (X,Y)) . (e,tv) is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[e,tv] is set
(FuncAdd (X,Y)) . [e,tv] is Relation-like Function-like set
[tseq,((FuncAdd (X,Y)) . (e,tv))] is Element of [:COMPLEX,(Funcs (X, the carrier of Y)):]
(X,Y) . [tseq,((FuncAdd (X,Y)) . (e,tv))] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
m is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
n is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
(FuncAdd (X,Y)) . (m,n) is set
[m,n] is set
(FuncAdd (X,Y)) . [m,n] is Relation-like Function-like set
m + (tseq * tseq) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . (m,(tseq * tseq)) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
[m,(tseq * tseq)] is set
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . [m,(tseq * tseq)] is set
f is complex set
tseq is complex set
f * tseq is complex set
tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
(f * tseq) * tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
tseq * tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
f * (tseq * tseq) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,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)
[(f * tseq),tseq] is set
(X,Y) . [(f * tseq),tseq] is Relation-like Function-like set
[tseq,tseq] is set
(X,Y) . [tseq,tseq] is Relation-like Function-like set
[f,((X,Y) . [tseq,tseq])] is set
(X,Y) . [f,((X,Y) . [tseq,tseq])] is Relation-like Function-like set
[f,(tseq * tseq)] is set
(X,Y) . [f,(tseq * tseq)] is Relation-like Function-like set
f is complex set
tseq is complex set
f + tseq is complex set
tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
(f + tseq) * tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
f * tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
tseq * tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
(f * tseq) + (tseq * tseq) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) is non empty Relation-like [: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):] -defined the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) -valued Function-like total quasi_total Element of bool [:[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):], the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):]
[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):] is non empty set
[:[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):], the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):] is non empty set
bool [:[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):], the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):] is non empty set
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . ((f * tseq),(tseq * tseq)) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
[(f * tseq),(tseq * tseq)] is set
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . [(f * tseq),(tseq * tseq)] is set
tseq is complex Element of COMPLEX
e is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
[tseq,e] is Element of [:COMPLEX,(Funcs (X, the carrier of Y)):]
(X,Y) . [tseq,e] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
tv is complex Element of COMPLEX
[tv,e] is Element of [:COMPLEX,(Funcs (X, the carrier of Y)):]
(X,Y) . [tv,e] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
tseq + tv is complex Element of COMPLEX
(tseq + tv) * tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
[(tseq + tv),e] is Element of [:COMPLEX,(Funcs (X, the carrier of Y)):]
(X,Y) . [(tseq + tv),e] is Relation-like X -defined the carrier of Y -valued Function-like total quasi_total Element of Funcs (X, the carrier of Y)
m is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
n is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
(FuncAdd (X,Y)) . (m,n) is set
[m,n] is set
(FuncAdd (X,Y)) . [m,n] is Relation-like Function-like set
tv * tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
m + (tv * tseq) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . (m,(tv * tseq)) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
[m,(tv * tseq)] is set
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . [m,(tv * tseq)] is set
tseq * tseq is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
(tseq * tseq) + (tv * tseq) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . ((tseq * tseq),(tv * tseq)) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
[(tseq * tseq),(tv * tseq)] is set
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) . [(tseq * tseq),(tv * tseq)] is set
0. CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) is zero Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
the ZeroF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
f is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
f + (0. CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)) is Element of the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #)
the addF of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) is non empty Relation-like [: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):] -defined the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #) -valued Function-like total quasi_total Element of bool [:[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):], the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #):]
[: the carrier of CLSStruct(# (Funcs (X, the carrier of Y)),(FuncZero (X,Y)),(FuncAdd (X,Y)),(X,Y) #), the carrier of CLSStruct(# (Funcs (X</