:: 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₁(X) is Element of the U1 of X
((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₁(X) is Element of the U1 of X
(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 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),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(