:: CLOPBAN1 semantic presentation

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