:: CLVECT_3 semantic presentation

REAL is V1() V47() V59() V60() V61() V65() set

NAT is V1() V4() V5() V6() V59() V60() V61() V62() V63() V64() V65() Element of K6(REAL)

K6(REAL) is set

COMPLEX is V1() V47() V59() V65() set

NAT is V1() V4() V5() V6() V59() V60() V61() V62() V63() V64() V65() set

K6(NAT) is set

K6(NAT) is set

RAT is V1() V47() V59() V60() V61() V62() V65() set

INT is V1() V47() V59() V60() V61() V62() V63() V65() set

K7(NAT,REAL) is complex-valued ext-real-valued real-valued set

K6(K7(NAT,REAL)) is set

K7(NAT,COMPLEX) is complex-valued set

K6(K7(NAT,COMPLEX)) is set

the_set_of_ComplexSequences is V1() set

K7(the_set_of_ComplexSequences,the_set_of_ComplexSequences) is set

K7(K7(the_set_of_ComplexSequences,the_set_of_ComplexSequences),the_set_of_ComplexSequences) is set

K6(K7(K7(the_set_of_ComplexSequences,the_set_of_ComplexSequences),the_set_of_ComplexSequences)) is set

K7(COMPLEX,the_set_of_ComplexSequences) is set

K7(K7(COMPLEX,the_set_of_ComplexSequences),the_set_of_ComplexSequences) is set

K6(K7(K7(COMPLEX,the_set_of_ComplexSequences),the_set_of_ComplexSequences)) is set

Linear_Space_of_ComplexSequences is V75() strict L17()

the U1 of Linear_Space_of_ComplexSequences is V1() set

K6( the U1 of Linear_Space_of_ComplexSequences) is set

the_set_of_l2ComplexSequences is Element of K6( the U1 of Linear_Space_of_ComplexSequences)

K7(the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences) is set

K7(K7(the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences),COMPLEX) is complex-valued set

K6(K7(K7(the_set_of_l2ComplexSequences,the_set_of_l2ComplexSequences),COMPLEX)) is set

0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative integer V59() V60() V61() V62() V63() V64() V65() set

1 is V1() V4() V5() V6() V10() V11() V12() ext-real positive non negative integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative integer V58() V59() V60() V61() V62() V63() V64() V65() Element of NAT

1r is V11() Element of COMPLEX

- 1r is V11() Element of COMPLEX

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums seq) + (Partial_Sums Cseq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

seq + Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums (seq + Cseq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

k + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

((Partial_Sums seq) + (Partial_Sums Cseq)) . (k + 1) is Element of the U1 of X

(Partial_Sums seq) . (k + 1) is Element of the U1 of X

(Partial_Sums Cseq) . (k + 1) is Element of the U1 of X

((Partial_Sums seq) . (k + 1)) + ((Partial_Sums Cseq) . (k + 1)) is Element of the U1 of X

(Partial_Sums seq) . k is Element of the U1 of X

seq . (k + 1) is Element of the U1 of X

((Partial_Sums seq) . k) + (seq . (k + 1)) is Element of the U1 of X

(((Partial_Sums seq) . k) + (seq . (k + 1))) + ((Partial_Sums Cseq) . (k + 1)) is Element of the U1 of X

Cseq . (k + 1) is Element of the U1 of X

(Partial_Sums Cseq) . k is Element of the U1 of X

(Cseq . (k + 1)) + ((Partial_Sums Cseq) . k) is Element of the U1 of X

(((Partial_Sums seq) . k) + (seq . (k + 1))) + ((Cseq . (k + 1)) + ((Partial_Sums Cseq) . k)) is Element of the U1 of X

(((Partial_Sums seq) . k) + (seq . (k + 1))) + (Cseq . (k + 1)) is Element of the U1 of X

((((Partial_Sums seq) . k) + (seq . (k + 1))) + (Cseq . (k + 1))) + ((Partial_Sums Cseq) . k) is Element of the U1 of X

(seq . (k + 1)) + (Cseq . (k + 1)) is Element of the U1 of X

((Partial_Sums seq) . k) + ((seq . (k + 1)) + (Cseq . (k + 1))) is Element of the U1 of X

(((Partial_Sums seq) . k) + ((seq . (k + 1)) + (Cseq . (k + 1)))) + ((Partial_Sums Cseq) . k) is Element of the U1 of X

(seq + Cseq) . (k + 1) is Element of the U1 of X

((Partial_Sums seq) . k) + ((seq + Cseq) . (k + 1)) is Element of the U1 of X

(((Partial_Sums seq) . k) + ((seq + Cseq) . (k + 1))) + ((Partial_Sums Cseq) . k) is Element of the U1 of X

((Partial_Sums seq) . k) + ((Partial_Sums Cseq) . k) is Element of the U1 of X

(((Partial_Sums seq) . k) + ((Partial_Sums Cseq) . k)) + ((seq + Cseq) . (k + 1)) is Element of the U1 of X

((Partial_Sums seq) + (Partial_Sums Cseq)) . k is Element of the U1 of X

(((Partial_Sums seq) + (Partial_Sums Cseq)) . k) + ((seq + Cseq) . (k + 1)) is Element of the U1 of X

((Partial_Sums seq) + (Partial_Sums Cseq)) . 0 is Element of the U1 of X

(Partial_Sums seq) . 0 is Element of the U1 of X

(Partial_Sums Cseq) . 0 is Element of the U1 of X

((Partial_Sums seq) . 0) + ((Partial_Sums Cseq) . 0) is Element of the U1 of X

seq . 0 is Element of the U1 of X

(seq . 0) + ((Partial_Sums Cseq) . 0) is Element of the U1 of X

Cseq . 0 is Element of the U1 of X

(seq . 0) + (Cseq . 0) is Element of the U1 of X

(seq + Cseq) . 0 is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums seq) - (Partial_Sums Cseq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

seq - Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums (seq - Cseq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

k + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

((Partial_Sums seq) - (Partial_Sums Cseq)) . (k + 1) is Element of the U1 of X

(Partial_Sums seq) . (k + 1) is Element of the U1 of X

(Partial_Sums Cseq) . (k + 1) is Element of the U1 of X

((Partial_Sums seq) . (k + 1)) - ((Partial_Sums Cseq) . (k + 1)) is Element of the U1 of X

- ((Partial_Sums Cseq) . (k + 1)) is Element of the U1 of X

K298(X,((Partial_Sums seq) . (k + 1)),(- ((Partial_Sums Cseq) . (k + 1)))) is Element of the U1 of X

(Partial_Sums seq) . k is Element of the U1 of X

seq . (k + 1) is Element of the U1 of X

((Partial_Sums seq) . k) + (seq . (k + 1)) is Element of the U1 of X

(((Partial_Sums seq) . k) + (seq . (k + 1))) - ((Partial_Sums Cseq) . (k + 1)) is Element of the U1 of X

K298(X,(((Partial_Sums seq) . k) + (seq . (k + 1))),(- ((Partial_Sums Cseq) . (k + 1)))) is Element of the U1 of X

Cseq . (k + 1) is Element of the U1 of X

(Partial_Sums Cseq) . k is Element of the U1 of X

(Cseq . (k + 1)) + ((Partial_Sums Cseq) . k) is Element of the U1 of X

(((Partial_Sums seq) . k) + (seq . (k + 1))) - ((Cseq . (k + 1)) + ((Partial_Sums Cseq) . k)) is Element of the U1 of X

- ((Cseq . (k + 1)) + ((Partial_Sums Cseq) . k)) is Element of the U1 of X

K298(X,(((Partial_Sums seq) . k) + (seq . (k + 1))),(- ((Cseq . (k + 1)) + ((Partial_Sums Cseq) . k)))) is Element of the U1 of X

(((Partial_Sums seq) . k) + (seq . (k + 1))) - (Cseq . (k + 1)) is Element of the U1 of X

- (Cseq . (k + 1)) is Element of the U1 of X

K298(X,(((Partial_Sums seq) . k) + (seq . (k + 1))),(- (Cseq . (k + 1)))) is Element of the U1 of X

((((Partial_Sums seq) . k) + (seq . (k + 1))) - (Cseq . (k + 1))) - ((Partial_Sums Cseq) . k) is Element of the U1 of X

- ((Partial_Sums Cseq) . k) is Element of the U1 of X

K298(X,((((Partial_Sums seq) . k) + (seq . (k + 1))) - (Cseq . (k + 1))),(- ((Partial_Sums Cseq) . k))) is Element of the U1 of X

(seq . (k + 1)) - (Cseq . (k + 1)) is Element of the U1 of X

K298(X,(seq . (k + 1)),(- (Cseq . (k + 1)))) is Element of the U1 of X

((Partial_Sums seq) . k) + ((seq . (k + 1)) - (Cseq . (k + 1))) is Element of the U1 of X

(((Partial_Sums seq) . k) + ((seq . (k + 1)) - (Cseq . (k + 1)))) - ((Partial_Sums Cseq) . k) is Element of the U1 of X

K298(X,(((Partial_Sums seq) . k) + ((seq . (k + 1)) - (Cseq . (k + 1)))),(- ((Partial_Sums Cseq) . k))) is Element of the U1 of X

((Partial_Sums seq) . k) - ((Partial_Sums Cseq) . k) is Element of the U1 of X

K298(X,((Partial_Sums seq) . k),(- ((Partial_Sums Cseq) . k))) is Element of the U1 of X

(((Partial_Sums seq) . k) - ((Partial_Sums Cseq) . k)) + ((seq . (k + 1)) - (Cseq . (k + 1))) is Element of the U1 of X

((Partial_Sums seq) - (Partial_Sums Cseq)) . k is Element of the U1 of X

(((Partial_Sums seq) - (Partial_Sums Cseq)) . k) + ((seq . (k + 1)) - (Cseq . (k + 1))) is Element of the U1 of X

(seq - Cseq) . (k + 1) is Element of the U1 of X

(((Partial_Sums seq) - (Partial_Sums Cseq)) . k) + ((seq - Cseq) . (k + 1)) is Element of the U1 of X

((Partial_Sums seq) - (Partial_Sums Cseq)) . 0 is Element of the U1 of X

(Partial_Sums seq) . 0 is Element of the U1 of X

(Partial_Sums Cseq) . 0 is Element of the U1 of X

((Partial_Sums seq) . 0) - ((Partial_Sums Cseq) . 0) is Element of the U1 of X

- ((Partial_Sums Cseq) . 0) is Element of the U1 of X

K298(X,((Partial_Sums seq) . 0),(- ((Partial_Sums Cseq) . 0))) is Element of the U1 of X

seq . 0 is Element of the U1 of X

(seq . 0) - ((Partial_Sums Cseq) . 0) is Element of the U1 of X

K298(X,(seq . 0),(- ((Partial_Sums Cseq) . 0))) is Element of the U1 of X

Cseq . 0 is Element of the U1 of X

(seq . 0) - (Cseq . 0) is Element of the U1 of X

- (Cseq . 0) is Element of the U1 of X

K298(X,(seq . 0),(- (Cseq . 0))) is Element of the U1 of X

(seq - Cseq) . 0 is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq is V11() set

Cseq * seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums (Cseq * seq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq * (Partial_Sums seq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

k + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(Cseq * (Partial_Sums seq)) . (k + 1) is Element of the U1 of X

(Partial_Sums seq) . (k + 1) is Element of the U1 of X

Cseq * ((Partial_Sums seq) . (k + 1)) is Element of the U1 of X

(Partial_Sums seq) . k is Element of the U1 of X

seq . (k + 1) is Element of the U1 of X

((Partial_Sums seq) . k) + (seq . (k + 1)) is Element of the U1 of X

Cseq * (((Partial_Sums seq) . k) + (seq . (k + 1))) is Element of the U1 of X

Cseq * ((Partial_Sums seq) . k) is Element of the U1 of X

Cseq * (seq . (k + 1)) is Element of the U1 of X

(Cseq * ((Partial_Sums seq) . k)) + (Cseq * (seq . (k + 1))) is Element of the U1 of X

(Cseq * (Partial_Sums seq)) . k is Element of the U1 of X

((Cseq * (Partial_Sums seq)) . k) + (Cseq * (seq . (k + 1))) is Element of the U1 of X

(Cseq * seq) . (k + 1) is Element of the U1 of X

((Cseq * (Partial_Sums seq)) . k) + ((Cseq * seq) . (k + 1)) is Element of the U1 of X

(Cseq * (Partial_Sums seq)) . 0 is Element of the U1 of X

(Partial_Sums seq) . 0 is Element of the U1 of X

Cseq * ((Partial_Sums seq) . 0) is Element of the U1 of X

seq . 0 is Element of the U1 of X

Cseq * (seq . 0) is Element of the U1 of X

(Cseq * seq) . 0 is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

- seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums (- seq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

- (Partial_Sums seq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(- 1r) * seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums ((- 1r) * seq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(- 1r) * (Partial_Sums seq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

n is V11() set

n * (Partial_Sums seq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

n * seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

k is V11() set

k * (Partial_Sums Cseq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(n * (Partial_Sums seq)) + (k * (Partial_Sums Cseq)) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

k * Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(n * seq) + (k * Cseq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums ((n * seq) + (k * Cseq)) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums (n * seq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums (n * seq)) + (k * (Partial_Sums Cseq)) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums (k * Cseq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums (n * seq)) + (Partial_Sums (k * Cseq)) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

lim (Partial_Sums seq) is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(X,seq) is Element of the U1 of X

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

lim (Partial_Sums seq) is Element of the U1 of X

Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

seq + Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(X,(seq + Cseq)) is Element of the U1 of X

Partial_Sums (seq + Cseq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

lim (Partial_Sums (seq + Cseq)) is Element of the U1 of X

(X,Cseq) is Element of the U1 of X

Partial_Sums Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

lim (Partial_Sums Cseq) is Element of the U1 of X

(X,seq) + (X,Cseq) is Element of the U1 of X

(Partial_Sums seq) + (Partial_Sums Cseq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

lim ((Partial_Sums seq) + (Partial_Sums Cseq)) is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(X,seq) is Element of the U1 of X

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

lim (Partial_Sums seq) is Element of the U1 of X

Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

seq - Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(X,(seq - Cseq)) is Element of the U1 of X

Partial_Sums (seq - Cseq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

lim (Partial_Sums (seq - Cseq)) is Element of the U1 of X

(X,Cseq) is Element of the U1 of X

Partial_Sums Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

lim (Partial_Sums Cseq) is Element of the U1 of X

(X,seq) - (X,Cseq) is Element of the U1 of X

- (X,Cseq) is Element of the U1 of X

K298(X,(X,seq),(- (X,Cseq))) is Element of the U1 of X

(Partial_Sums seq) - (Partial_Sums Cseq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

lim ((Partial_Sums seq) - (Partial_Sums Cseq)) is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(X,seq) is Element of the U1 of X

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

lim (Partial_Sums seq) is Element of the U1 of X

Cseq is V11() set

Cseq * seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(X,(Cseq * seq)) is Element of the U1 of X

Partial_Sums (Cseq * seq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

lim (Partial_Sums (Cseq * seq)) is Element of the U1 of X

Cseq * (X,seq) is Element of the U1 of X

Cseq * (Partial_Sums seq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

lim (Cseq * (Partial_Sums seq)) is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

0. X is V82(X) Element of the U1 of X

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

lim seq is Element of the U1 of X

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

n + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(Partial_Sums seq) . (n + 1) is Element of the U1 of X

(Partial_Sums seq) . n is Element of the U1 of X

seq . (n + 1) is Element of the U1 of X

((Partial_Sums seq) . n) + (seq . (n + 1)) is Element of the U1 of X

seq ^\ 1 is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) subsequence of seq

(seq ^\ 1) . n is Element of the U1 of X

((Partial_Sums seq) . n) + ((seq ^\ 1) . n) is Element of the U1 of X

(Partial_Sums seq) ^\ 1 is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) subsequence of Partial_Sums seq

((Partial_Sums seq) ^\ 1) . n is Element of the U1 of X

(Partial_Sums seq) + (seq ^\ 1) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums seq) - (Partial_Sums seq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq)) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

((seq ^\ 1) + ((Partial_Sums seq) - (Partial_Sums seq))) . n is Element of the U1 of X

(seq ^\ 1) . n is Element of the U1 of X

((Partial_Sums seq) - (Partial_Sums seq)) . n is Element of the U1 of X

((seq ^\ 1) . n) + (((Partial_Sums seq) - (Partial_Sums seq)) . n) is Element of the U1 of X

(Partial_Sums seq) . n is Element of the U1 of X

((Partial_Sums seq) . n) - ((Partial_Sums seq) . n) is Element of the U1 of X

- ((Partial_Sums seq) . n) is Element of the U1 of X

K298(X,((Partial_Sums seq) . n),(- ((Partial_Sums seq) . n))) is Element of the U1 of X

((seq ^\ 1) . n) + (((Partial_Sums seq) . n) - ((Partial_Sums seq) . n)) is Element of the U1 of X

((seq ^\ 1) . n) + H

((Partial_Sums seq) ^\ 1) - (Partial_Sums seq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

lim ((Partial_Sums seq) ^\ 1) is Element of the U1 of X

lim (Partial_Sums seq) is Element of the U1 of X

lim (((Partial_Sums seq) ^\ 1) - (Partial_Sums seq)) is Element of the U1 of X

(lim (Partial_Sums seq)) - (lim (Partial_Sums seq)) is Element of the U1 of X

- (lim (Partial_Sums seq)) is Element of the U1 of X

K298(X,(lim (Partial_Sums seq)),(- (lim (Partial_Sums seq)))) is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like V160() CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

n is V11() V12() ext-real Element of REAL

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq . 0 is Element of the U1 of X

Cseq ^\ 1 is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) subsequence of Cseq

Partial_Sums (Cseq ^\ 1) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums Cseq) ^\ 1 is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) subsequence of Partial_Sums Cseq

((Partial_Sums Cseq) ^\ 1) - seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

n + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(((Partial_Sums Cseq) ^\ 1) - seq) . (n + 1) is Element of the U1 of X

((Partial_Sums Cseq) ^\ 1) . (n + 1) is Element of the U1 of X

seq . (n + 1) is Element of the U1 of X

(((Partial_Sums Cseq) ^\ 1) . (n + 1)) - (seq . (n + 1)) is Element of the U1 of X

- (seq . (n + 1)) is Element of the U1 of X

K298(X,(((Partial_Sums Cseq) ^\ 1) . (n + 1)),(- (seq . (n + 1)))) is Element of the U1 of X

(((Partial_Sums Cseq) ^\ 1) . (n + 1)) - (Cseq . 0) is Element of the U1 of X

- (Cseq . 0) is Element of the U1 of X

K298(X,(((Partial_Sums Cseq) ^\ 1) . (n + 1)),(- (Cseq . 0))) is Element of the U1 of X

(n + 1) + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(Partial_Sums Cseq) . ((n + 1) + 1) is Element of the U1 of X

((Partial_Sums Cseq) . ((n + 1) + 1)) - (Cseq . 0) is Element of the U1 of X

K298(X,((Partial_Sums Cseq) . ((n + 1) + 1)),(- (Cseq . 0))) is Element of the U1 of X

Cseq . ((n + 1) + 1) is Element of the U1 of X

(Partial_Sums Cseq) . (n + 1) is Element of the U1 of X

(Cseq . ((n + 1) + 1)) + ((Partial_Sums Cseq) . (n + 1)) is Element of the U1 of X

((Cseq . ((n + 1) + 1)) + ((Partial_Sums Cseq) . (n + 1))) - (Cseq . 0) is Element of the U1 of X

K298(X,((Cseq . ((n + 1) + 1)) + ((Partial_Sums Cseq) . (n + 1))),(- (Cseq . 0))) is Element of the U1 of X

seq . n is Element of the U1 of X

((Cseq . ((n + 1) + 1)) + ((Partial_Sums Cseq) . (n + 1))) - (seq . n) is Element of the U1 of X

- (seq . n) is Element of the U1 of X

K298(X,((Cseq . ((n + 1) + 1)) + ((Partial_Sums Cseq) . (n + 1))),(- (seq . n))) is Element of the U1 of X

((Partial_Sums Cseq) . (n + 1)) - (seq . n) is Element of the U1 of X

K298(X,((Partial_Sums Cseq) . (n + 1)),(- (seq . n))) is Element of the U1 of X

(Cseq . ((n + 1) + 1)) + (((Partial_Sums Cseq) . (n + 1)) - (seq . n)) is Element of the U1 of X

((Partial_Sums Cseq) ^\ 1) . n is Element of the U1 of X

(((Partial_Sums Cseq) ^\ 1) . n) - (seq . n) is Element of the U1 of X

K298(X,(((Partial_Sums Cseq) ^\ 1) . n),(- (seq . n))) is Element of the U1 of X

(Cseq . ((n + 1) + 1)) + ((((Partial_Sums Cseq) ^\ 1) . n) - (seq . n)) is Element of the U1 of X

(((Partial_Sums Cseq) ^\ 1) - seq) . n is Element of the U1 of X

(Cseq . ((n + 1) + 1)) + ((((Partial_Sums Cseq) ^\ 1) - seq) . n) is Element of the U1 of X

(Cseq ^\ 1) . (n + 1) is Element of the U1 of X

((((Partial_Sums Cseq) ^\ 1) - seq) . n) + ((Cseq ^\ 1) . (n + 1)) is Element of the U1 of X

(((Partial_Sums Cseq) ^\ 1) - seq) . 0 is Element of the U1 of X

((Partial_Sums Cseq) ^\ 1) . 0 is Element of the U1 of X

seq . 0 is Element of the U1 of X

(((Partial_Sums Cseq) ^\ 1) . 0) - (seq . 0) is Element of the U1 of X

- (seq . 0) is Element of the U1 of X

K298(X,(((Partial_Sums Cseq) ^\ 1) . 0),(- (seq . 0))) is Element of the U1 of X

(((Partial_Sums Cseq) ^\ 1) . 0) - (Cseq . 0) is Element of the U1 of X

K298(X,(((Partial_Sums Cseq) ^\ 1) . 0),(- (Cseq . 0))) is Element of the U1 of X

0 + 1 is V1() V4() V5() V6() V10() V11() V12() ext-real positive non negative integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(Partial_Sums Cseq) . (0 + 1) is Element of the U1 of X

((Partial_Sums Cseq) . (0 + 1)) - (Cseq . 0) is Element of the U1 of X

K298(X,((Partial_Sums Cseq) . (0 + 1)),(- (Cseq . 0))) is Element of the U1 of X

(Partial_Sums Cseq) . 0 is Element of the U1 of X

Cseq . (0 + 1) is Element of the U1 of X

((Partial_Sums Cseq) . 0) + (Cseq . (0 + 1)) is Element of the U1 of X

(((Partial_Sums Cseq) . 0) + (Cseq . (0 + 1))) - (Cseq . 0) is Element of the U1 of X

K298(X,(((Partial_Sums Cseq) . 0) + (Cseq . (0 + 1))),(- (Cseq . 0))) is Element of the U1 of X

(Cseq . (0 + 1)) + (Cseq . 0) is Element of the U1 of X

((Cseq . (0 + 1)) + (Cseq . 0)) - (Cseq . 0) is Element of the U1 of X

K298(X,((Cseq . (0 + 1)) + (Cseq . 0)),(- (Cseq . 0))) is Element of the U1 of X

(Cseq . 0) - (Cseq . 0) is Element of the U1 of X

K298(X,(Cseq . 0),(- (Cseq . 0))) is Element of the U1 of X

(Cseq . (0 + 1)) + ((Cseq . 0) - (Cseq . 0)) is Element of the U1 of X

0. X is V82(X) Element of the U1 of X

(Cseq . (0 + 1)) + H

(Cseq ^\ 1) . 0 is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

seq ^\ Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) subsequence of seq

Cseq + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

seq ^\ (Cseq + 1) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) subsequence of seq

(seq ^\ Cseq) . 0 is Element of the U1 of X

NAT --> ((seq ^\ Cseq) . 0) is V1() V13() V16( NAT ) V17( the U1 of X) V18() constant V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums (seq ^\ Cseq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums (seq ^\ Cseq)) ^\ 1 is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) subsequence of Partial_Sums (seq ^\ Cseq)

n is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

n . k is Element of the U1 of X

(seq ^\ Cseq) ^\ 1 is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) subsequence of seq ^\ Cseq

Partial_Sums ((seq ^\ Cseq) ^\ 1) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

((Partial_Sums (seq ^\ Cseq)) ^\ 1) - n is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

seq ^\ 0 is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) subsequence of seq

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

seq ^\ Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) subsequence of seq

(seq ^\ Cseq) ^\ 1 is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) subsequence of seq ^\ Cseq

Partial_Sums ((seq ^\ Cseq) ^\ 1) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums seq) . Cseq is Element of the U1 of X

NAT --> ((Partial_Sums seq) . Cseq) is V1() V13() V16( NAT ) V17( the U1 of X) V18() constant V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(Partial_Sums seq) ^\ (Cseq + 1) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) subsequence of Partial_Sums seq

seq ^\ (Cseq + 1) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) subsequence of seq

Partial_Sums (seq ^\ (Cseq + 1)) is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

n is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums (seq ^\ (Cseq + 1))) . 0 is Element of the U1 of X

(seq ^\ (Cseq + 1)) . 0 is Element of the U1 of X

0 + (Cseq + 1) is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

seq . (0 + (Cseq + 1)) is Element of the U1 of X

seq . (Cseq + 1) is Element of the U1 of X

k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

((Partial_Sums seq) ^\ (Cseq + 1)) . k is Element of the U1 of X

(Partial_Sums (seq ^\ (Cseq + 1))) . k is Element of the U1 of X

n . k is Element of the U1 of X

((Partial_Sums (seq ^\ (Cseq + 1))) . k) + (n . k) is Element of the U1 of X

k + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(Partial_Sums (seq ^\ (Cseq + 1))) . (k + 1) is Element of the U1 of X

n . (k + 1) is Element of the U1 of X

((Partial_Sums (seq ^\ (Cseq + 1))) . (k + 1)) + (n . (k + 1)) is Element of the U1 of X

(seq ^\ (Cseq + 1)) . (k + 1) is Element of the U1 of X

((Partial_Sums (seq ^\ (Cseq + 1))) . k) + ((seq ^\ (Cseq + 1)) . (k + 1)) is Element of the U1 of X

(n . (k + 1)) + (((Partial_Sums (seq ^\ (Cseq + 1))) . k) + ((seq ^\ (Cseq + 1)) . (k + 1))) is Element of the U1 of X

(n . (k + 1)) + ((Partial_Sums (seq ^\ (Cseq + 1))) . k) is Element of the U1 of X

((n . (k + 1)) + ((Partial_Sums (seq ^\ (Cseq + 1))) . k)) + ((seq ^\ (Cseq + 1)) . (k + 1)) is Element of the U1 of X

((Partial_Sums seq) . Cseq) + ((Partial_Sums (seq ^\ (Cseq + 1))) . k) is Element of the U1 of X

(((Partial_Sums seq) . Cseq) + ((Partial_Sums (seq ^\ (Cseq + 1))) . k)) + ((seq ^\ (Cseq + 1)) . (k + 1)) is Element of the U1 of X

(((Partial_Sums seq) ^\ (Cseq + 1)) . k) + ((seq ^\ (Cseq + 1)) . (k + 1)) is Element of the U1 of X

k + (Cseq + 1) is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(Partial_Sums seq) . (k + (Cseq + 1)) is Element of the U1 of X

((Partial_Sums seq) . (k + (Cseq + 1))) + ((seq ^\ (Cseq + 1)) . (k + 1)) is Element of the U1 of X

(k + 1) + (Cseq + 1) is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

seq . ((k + 1) + (Cseq + 1)) is Element of the U1 of X

((Partial_Sums seq) . (k + (Cseq + 1))) + (seq . ((k + 1) + (Cseq + 1))) is Element of the U1 of X

(k + (Cseq + 1)) + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(Partial_Sums seq) . ((k + (Cseq + 1)) + 1) is Element of the U1 of X

(Partial_Sums seq) . ((k + 1) + (Cseq + 1)) is Element of the U1 of X

((Partial_Sums seq) ^\ (Cseq + 1)) . (k + 1) is Element of the U1 of X

((Partial_Sums seq) ^\ (Cseq + 1)) . 0 is Element of the U1 of X

(Partial_Sums seq) . (0 + (Cseq + 1)) is Element of the U1 of X

((Partial_Sums seq) . Cseq) + (seq . (Cseq + 1)) is Element of the U1 of X

n . 0 is Element of the U1 of X

((Partial_Sums (seq ^\ (Cseq + 1))) . 0) + (n . 0) is Element of the U1 of X

(Partial_Sums (seq ^\ (Cseq + 1))) + n is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums ((seq ^\ Cseq) ^\ 1)) + n is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(Partial_Sums seq) . Cseq is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(X,seq,0) is Element of the U1 of X

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums seq) . 0 is Element of the U1 of X

seq . 0 is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(X,seq,1) is Element of the U1 of X

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums seq) . 1 is Element of the U1 of X

(X,seq,0) is Element of the U1 of X

(Partial_Sums seq) . 0 is Element of the U1 of X

seq . 1 is Element of the U1 of X

(X,seq,0) + (seq . 1) is Element of the U1 of X

0 + 1 is V1() V4() V5() V6() V10() V11() V12() ext-real positive non negative integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

seq . (0 + 1) is Element of the U1 of X

((Partial_Sums seq) . 0) + (seq . (0 + 1)) is Element of the U1 of X

((Partial_Sums seq) . 0) + (seq . 1) is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(X,seq,1) is Element of the U1 of X

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums seq) . 1 is Element of the U1 of X

seq . 0 is Element of the U1 of X

seq . 1 is Element of the U1 of X

(seq . 0) + (seq . 1) is Element of the U1 of X

(X,seq,0) is Element of the U1 of X

(Partial_Sums seq) . 0 is Element of the U1 of X

(X,seq,0) + (seq . 1) is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

Cseq + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(X,seq,(Cseq + 1)) is Element of the U1 of X

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums seq) . (Cseq + 1) is Element of the U1 of X

(X,seq,Cseq) is Element of the U1 of X

(Partial_Sums seq) . Cseq is Element of the U1 of X

seq . (Cseq + 1) is Element of the U1 of X

(X,seq,Cseq) + (seq . (Cseq + 1)) is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

Cseq + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

seq . (Cseq + 1) is Element of the U1 of X

(X,seq,(Cseq + 1)) is Element of the U1 of X

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums seq) . (Cseq + 1) is Element of the U1 of X

(X,seq,Cseq) is Element of the U1 of X

(Partial_Sums seq) . Cseq is Element of the U1 of X

(X,seq,(Cseq + 1)) - (X,seq,Cseq) is Element of the U1 of X

- (X,seq,Cseq) is Element of the U1 of X

K298(X,(X,seq,(Cseq + 1)),(- (X,seq,Cseq))) is Element of the U1 of X

(seq . (Cseq + 1)) + (X,seq,Cseq) is Element of the U1 of X

((seq . (Cseq + 1)) + (X,seq,Cseq)) - (X,seq,Cseq) is Element of the U1 of X

K298(X,((seq . (Cseq + 1)) + (X,seq,Cseq)),(- (X,seq,Cseq))) is Element of the U1 of X

(X,seq,Cseq) - (X,seq,Cseq) is Element of the U1 of X

K298(X,(X,seq,Cseq),(- (X,seq,Cseq))) is Element of the U1 of X

(seq . (Cseq + 1)) + ((X,seq,Cseq) - (X,seq,Cseq)) is Element of the U1 of X

0. X is V82(X) Element of the U1 of X

(seq . (Cseq + 1)) + (0. X) is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

seq . 1 is Element of the U1 of X

(X,seq,1) is Element of the U1 of X

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums seq) . 1 is Element of the U1 of X

(X,seq,0) is Element of the U1 of X

(Partial_Sums seq) . 0 is Element of the U1 of X

(X,seq,1) - (X,seq,0) is Element of the U1 of X

- (X,seq,0) is Element of the U1 of X

K298(X,(X,seq,1),(- (X,seq,0))) is Element of the U1 of X

0 + 1 is V1() V4() V5() V6() V10() V11() V12() ext-real positive non negative integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

seq . (0 + 1) is Element of the U1 of X

(X,seq,(0 + 1)) is Element of the U1 of X

(Partial_Sums seq) . (0 + 1) is Element of the U1 of X

(X,seq,(0 + 1)) - (X,seq,0) is Element of the U1 of X

K298(X,(X,seq,(0 + 1)),(- (X,seq,0))) is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(X,seq,Cseq) is Element of the U1 of X

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums seq) . Cseq is Element of the U1 of X

n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(X,seq,n) is Element of the U1 of X

(Partial_Sums seq) . n is Element of the U1 of X

(X,seq,Cseq) - (X,seq,n) is Element of the U1 of X

- (X,seq,n) is Element of the U1 of X

K298(X,(X,seq,Cseq),(- (X,seq,n))) is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(X,seq,1,0) is Element of the U1 of X

(X,seq,1) is Element of the U1 of X

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums seq) . 1 is Element of the U1 of X

(X,seq,0) is Element of the U1 of X

(Partial_Sums seq) . 0 is Element of the U1 of X

(X,seq,1) - (X,seq,0) is Element of the U1 of X

- (X,seq,0) is Element of the U1 of X

K298(X,(X,seq,1),(- (X,seq,0))) is Element of the U1 of X

seq . 1 is Element of the U1 of X

seq . 0 is Element of the U1 of X

(seq . 0) + (seq . 1) is Element of the U1 of X

((seq . 0) + (seq . 1)) - (X,seq,0) is Element of the U1 of X

K298(X,((seq . 0) + (seq . 1)),(- (X,seq,0))) is Element of the U1 of X

(seq . 1) + (seq . 0) is Element of the U1 of X

((seq . 1) + (seq . 0)) - (seq . 0) is Element of the U1 of X

- (seq . 0) is Element of the U1 of X

K298(X,((seq . 1) + (seq . 0)),(- (seq . 0))) is Element of the U1 of X

(seq . 0) - (seq . 0) is Element of the U1 of X

K298(X,(seq . 0),(- (seq . 0))) is Element of the U1 of X

(seq . 1) + ((seq . 0) - (seq . 0)) is Element of the U1 of X

0. X is V82(X) Element of the U1 of X

(seq . 1) + H

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

Cseq + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(X,seq,(Cseq + 1),Cseq) is Element of the U1 of X

(X,seq,(Cseq + 1)) is Element of the U1 of X

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums seq) . (Cseq + 1) is Element of the U1 of X

(X,seq,Cseq) is Element of the U1 of X

(Partial_Sums seq) . Cseq is Element of the U1 of X

(X,seq,(Cseq + 1)) - (X,seq,Cseq) is Element of the U1 of X

- (X,seq,Cseq) is Element of the U1 of X

K298(X,(X,seq,(Cseq + 1)),(- (X,seq,Cseq))) is Element of the U1 of X

seq . (Cseq + 1) is Element of the U1 of X

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like V160() CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq is V11() V12() ext-real Element of REAL

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

m2 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(X,seq,k) is Element of the U1 of X

(Partial_Sums seq) . k is Element of the U1 of X

(X,seq,m2) is Element of the U1 of X

(Partial_Sums seq) . m2 is Element of the U1 of X

(X,seq,k) - (X,seq,m2) is Element of the U1 of X

- (X,seq,m2) is Element of the U1 of X

K298(X,(X,seq,k),(- (X,seq,m2))) is Element of the U1 of X

||.((X,seq,k) - (X,seq,m2)).|| is V11() V12() ext-real Element of REAL

Cseq is V11() V12() ext-real Element of REAL

Cseq is V11() V12() ext-real Element of REAL

n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

m2 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(X,seq,k) is Element of the U1 of X

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums seq) . k is Element of the U1 of X

(X,seq,m2) is Element of the U1 of X

(Partial_Sums seq) . m2 is Element of the U1 of X

(X,seq,k) - (X,seq,m2) is Element of the U1 of X

- (X,seq,m2) is Element of the U1 of X

K298(X,(X,seq,k),(- (X,seq,m2))) is Element of the U1 of X

||.((X,seq,k) - (X,seq,m2)).|| is V11() V12() ext-real Element of REAL

((Partial_Sums seq) . k) - ((Partial_Sums seq) . m2) is Element of the U1 of X

- ((Partial_Sums seq) . m2) is Element of the U1 of X

K298(X,((Partial_Sums seq) . k),(- ((Partial_Sums seq) . m2))) is Element of the U1 of X

||.(((Partial_Sums seq) . k) - ((Partial_Sums seq) . m2)).|| is V11() V12() ext-real Element of REAL

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like V160() CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq is V11() V12() ext-real Element of REAL

n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

m2 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(X,seq,k,m2) is Element of the U1 of X

(X,seq,k) is Element of the U1 of X

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums seq) . k is Element of the U1 of X

(X,seq,m2) is Element of the U1 of X

(Partial_Sums seq) . m2 is Element of the U1 of X

(X,seq,k) - (X,seq,m2) is Element of the U1 of X

- (X,seq,m2) is Element of the U1 of X

K298(X,(X,seq,k),(- (X,seq,m2))) is Element of the U1 of X

||.(X,seq,k,m2).|| is V11() V12() ext-real Element of REAL

Cseq is V11() V12() ext-real Element of REAL

Cseq is V11() V12() ext-real Element of REAL

n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

m2 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(X,seq,k,m2) is Element of the U1 of X

(X,seq,k) is Element of the U1 of X

Partial_Sums seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

(Partial_Sums seq) . k is Element of the U1 of X

(X,seq,m2) is Element of the U1 of X

(Partial_Sums seq) . m2 is Element of the U1 of X

(X,seq,k) - (X,seq,m2) is Element of the U1 of X

- (X,seq,m2) is Element of the U1 of X

K298(X,(X,seq,k),(- (X,seq,m2))) is Element of the U1 of X

||.(X,seq,k,m2).|| is V11() V12() ext-real Element of REAL

||.((X,seq,k) - (X,seq,m2)).|| is V11() V12() ext-real Element of REAL

X is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))

Partial_Sums X is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))

seq is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(Partial_Sums X) . seq is V11() Element of COMPLEX

X is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))

seq is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(X,seq) is V11() set

Partial_Sums X is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))

(Partial_Sums X) . seq is V11() Element of COMPLEX

Cseq is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

(X,Cseq) is V11() set

(Partial_Sums X) . Cseq is V11() Element of COMPLEX

(X,seq) - (X,Cseq) is V11() set

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

seq + Cseq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

||.(seq + Cseq).|| is V1() V13() V16( NAT ) V17( REAL ) V18() V23( NAT ) V27( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

||.seq.|| is V1() V13() V16( NAT ) V17( REAL ) V18() V23( NAT ) V27( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

||.Cseq.|| is V1() V13() V16( NAT ) V17( REAL ) V18() V23( NAT ) V27( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

||.seq.|| + ||.Cseq.|| is V1() V13() V16( NAT ) V17( REAL ) V18() V23( NAT ) V27( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))

n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT

||.(seq + Cseq).|| . n is V11() V12() ext-real Element of REAL

(||.seq.|| + ||.Cseq.||) . n is V11() V12() ext-real Element of REAL

(seq + Cseq) . n is Element of the U1 of X

||.((seq + Cseq) . n).|| is V11() V12() ext-real Element of REAL

seq . n is Element of the U1 of X

Cseq . n is Element of the U1 of X

(seq . n) + (Cseq . n) is Element of the U1 of X

||.((seq . n) + (Cseq . n)).|| is V11() V12() ext-real Element of REAL

||.(seq . n).|| is V11() V12() ext-real Element of REAL

||.(Cseq . n).|| is V11() V12() ext-real Element of REAL

||.(seq . n).|| + ||.(Cseq . n).|| is V11() V12() ext-real Element of REAL

||.seq.|| . n is V11() V12() ext-real Element of REAL

(||.seq.|| . n) + ||.(Cseq . n).|| is V11() V12() ext-real Element of REAL

||.Cseq.|| . n is V11() V12() ext-real Element of REAL

(||.seq.|| . n) + (||.Cseq.|| . n) is V11() V12() ext-real Element of REAL

X is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like CUNITSTR

the U1 of X is V1() set

K7(NAT, the U1 of X) is set

K6(K7(NAT, the U1 of X)) is set

seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(NAT, the U1 of X))

Cseq is V11() set

Cseq * seq is V1() V13() V16( NAT ) V17( the U1 of X) V18() V23( NAT ) V27( NAT , the U1 of X) Element of K6(K7(