:: 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(NAT, the U1 of X))
||.(Cseq * 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))
||.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 V11() V12() ext-real Element of REAL
|.Cseq.| (#) ||.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))
n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.(Cseq * seq).|| . n is V11() V12() ext-real Element of REAL
(|.Cseq.| (#) ||.seq.||) . n is V11() V12() ext-real Element of REAL
(Cseq * seq) . n is Element of the U1 of X
||.((Cseq * seq) . n).|| is V11() V12() ext-real Element of REAL
seq . n is Element of the U1 of X
Cseq * (seq . n) is Element of the U1 of X
||.(Cseq * (seq . n)).|| is V11() V12() ext-real Element of REAL
||.(seq . n).|| is V11() V12() ext-real Element of REAL
|.Cseq.| * ||.(seq . n).|| is V11() V12() ext-real Element of REAL
||.seq.|| . n is V11() V12() ext-real Element of REAL
|.Cseq.| * (||.seq.|| . 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))
||.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))
n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.seq.|| . n is V11() V12() ext-real Element of REAL
seq . n is Element of the U1 of X
||.(seq . 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
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))
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))
lim Cseq is V11() V12() ext-real Element of 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))
n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.seq.|| . n is V11() V12() ext-real Element of REAL
Cseq . n is V11() V12() ext-real Element of REAL
n + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.seq.|| . (n + 1) is V11() V12() ext-real Element of REAL
(||.seq.|| . (n + 1)) / (||.seq.|| . n) is V11() V12() ext-real Element of REAL
seq . n is Element of the U1 of X
||.(seq . n).|| is V11() V12() ext-real Element of REAL
seq . (n + 1) is Element of the U1 of X
||.(seq . (n + 1)).|| is V11() V12() ext-real Element of REAL
||.(seq . (n + 1)).|| / ||.(seq . n).|| is V11() V12() ext-real Element of REAL
(||.seq.|| . (n + 1)) / ||.(seq . 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
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
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
n + 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
seq . k is Element of the U1 of X
(seq . k) - H₁(X) is Element of the U1 of X
- (0. X) is Element of the U1 of X
K298(X,(seq . k),(- (0. X))) is Element of the U1 of X
||.((seq . k) - H₁(X)).|| is V11() V12() ext-real Element of REAL
||.(seq . k).|| 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
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))
Cseq is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq . Cseq is Element of the U1 of X
||.(seq . Cseq).|| is V11() V12() ext-real Element of REAL
k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Cseq + k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq . (Cseq + k) is Element of the U1 of X
||.(seq . (Cseq + k)).|| is V11() V12() ext-real Element of REAL
k + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Cseq + (k + 1) is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq . (Cseq + (k + 1)) is Element of the U1 of X
||.(seq . (Cseq + (k + 1))).|| is V11() V12() ext-real Element of REAL
(Cseq + k) + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq . ((Cseq + k) + 1) is Element of the U1 of X
||.(seq . ((Cseq + k) + 1)).|| is V11() V12() ext-real Element of REAL
||.(seq . ((Cseq + k) + 1)).|| / ||.(seq . (Cseq + k)).|| is V11() V12() ext-real Element of REAL
Cseq + 0 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq . (Cseq + 0) is Element of the U1 of X
||.(seq . (Cseq + 0)).|| 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 set
Cseq + k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq . n is Element of the U1 of X
||.(seq . n).|| is V11() V12() ext-real Element of REAL
lim 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))
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))
lim Cseq is V11() V12() ext-real Element of REAL
(lim Cseq) - 1 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
n + 1 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
Cseq . k is V11() V12() ext-real Element of REAL
k + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq . (k + 1) is Element of the U1 of X
||.(seq . (k + 1)).|| is V11() V12() ext-real Element of REAL
seq . k is Element of the U1 of X
||.(seq . k).|| is V11() V12() ext-real Element of REAL
||.(seq . (k + 1)).|| / ||.(seq . k).|| is V11() V12() ext-real Element of REAL
(||.(seq . (k + 1)).|| / ||.(seq . k).||) - (lim Cseq) is V11() V12() ext-real Element of REAL
abs ((||.(seq . (k + 1)).|| / ||.(seq . k).||) - (lim Cseq)) is V11() V12() ext-real Element of REAL
- ((lim Cseq) - 1) is V11() V12() ext-real Element of REAL
((||.(seq . (k + 1)).|| / ||.(seq . k).||) - (lim Cseq)) + (lim Cseq) is V11() V12() ext-real Element of REAL
1 - (lim Cseq) is V11() V12() ext-real Element of REAL
(1 - (lim Cseq)) + (lim Cseq) 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 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))
lim Cseq is V11() V12() ext-real Element of 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))
n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.seq.|| . n is V11() V12() ext-real Element of REAL
Cseq . n is V11() V12() ext-real Element of REAL
n -root (||.seq.|| . n) is V11() V12() ext-real Element of REAL
seq . n is Element of the U1 of X
||.(seq . n).|| is V11() V12() ext-real Element of REAL
n -root ||.(seq . 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))
||.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))
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
k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Cseq . k is V11() V12() ext-real Element of REAL
||.seq.|| . k is V11() V12() ext-real Element of REAL
k -root (||.seq.|| . k) is V11() V12() ext-real Element of REAL
seq . k is Element of the U1 of X
||.(seq . k).|| is V11() V12() ext-real Element of REAL
k -root ||.(seq . k).|| is V11() V12() ext-real Element of REAL
(k -root ||.(seq . k).||) |^ k is V11() V12() ext-real Element of REAL
lim seq is Element of the U1 of X
0. X is V82(X) 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( 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))
lim Cseq is V11() V12() ext-real Element of REAL
(lim Cseq) - 1 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
n + 1 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
Cseq . k is V11() V12() ext-real Element of REAL
||.seq.|| . k is V11() V12() ext-real Element of REAL
k -root (||.seq.|| . k) is V11() V12() ext-real Element of REAL
seq . k is Element of the U1 of X
||.(seq . k).|| is V11() V12() ext-real Element of REAL
k -root ||.(seq . k).|| is V11() V12() ext-real Element of REAL
(k -root ||.(seq . k).||) - (lim Cseq) is V11() V12() ext-real Element of REAL
abs ((k -root ||.(seq . k).||) - (lim Cseq)) is V11() V12() ext-real Element of REAL
- ((lim Cseq) - 1) is V11() V12() ext-real Element of REAL
((k -root ||.(seq . k).||) - (lim Cseq)) + (lim Cseq) is V11() V12() ext-real Element of REAL
1 - (lim Cseq) is V11() V12() ext-real Element of REAL
(1 - (lim Cseq)) + (lim Cseq) is V11() V12() ext-real Element of REAL
(k -root ||.(seq . k).||) |^ k is V11() V12() ext-real Element of REAL
lim seq is Element of the U1 of X
0. X is V82(X) 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( REAL ) V18() V23( NAT ) V27( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(NAT,REAL))
Partial_Sums ||.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 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
||.(seq . (Cseq + 1)).|| is V11() V12() ext-real Element of REAL
||.seq.|| . (Cseq + 1) is V11() V12() ext-real Element of REAL
(Partial_Sums ||.seq.||) . Cseq is V11() V12() ext-real Element of REAL
0 + ((Partial_Sums ||.seq.||) . Cseq) is V11() V12() ext-real Element of REAL
(||.seq.|| . (Cseq + 1)) + ((Partial_Sums ||.seq.||) . Cseq) is V11() V12() ext-real Element of REAL
(Partial_Sums ||.seq.||) . (Cseq + 1) 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))
||.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))
Partial_Sums ||.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 V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums ||.seq.||) . Cseq is V11() V12() ext-real Element of REAL
seq . 0 is Element of the U1 of X
||.(seq . 0).|| is V11() V12() ext-real Element of REAL
||.seq.|| . 0 is V11() V12() ext-real Element of REAL
(Partial_Sums ||.seq.||) . 0 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))
||.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))
Partial_Sums ||.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 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
(Partial_Sums seq) . (Cseq + 1) 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
((Partial_Sums seq) . Cseq) + (seq . (Cseq + 1)) is Element of the U1 of X
||.((Partial_Sums seq) . (Cseq + 1)).|| is V11() V12() ext-real Element of REAL
||.((Partial_Sums seq) . Cseq).|| is V11() V12() ext-real Element of REAL
||.(seq . (Cseq + 1)).|| is V11() V12() ext-real Element of REAL
||.((Partial_Sums seq) . Cseq).|| + ||.(seq . (Cseq + 1)).|| is V11() V12() ext-real Element of REAL
(Partial_Sums ||.seq.||) . Cseq is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . Cseq) + ||.(seq . (Cseq + 1)).|| is V11() V12() ext-real Element of REAL
||.seq.|| . (Cseq + 1) is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . Cseq) + (||.seq.|| . (Cseq + 1)) is V11() V12() ext-real Element of REAL
(Partial_Sums ||.seq.||) . (Cseq + 1) is V11() V12() ext-real Element of REAL
(Partial_Sums ||.seq.||) . 0 is V11() V12() ext-real Element of REAL
||.seq.|| . 0 is V11() V12() ext-real Element of REAL
seq . 0 is Element of the U1 of X
||.(seq . 0).|| is V11() V12() ext-real Element of REAL
(Partial_Sums seq) . 0 is Element of the U1 of X
||.((Partial_Sums seq) . 0).|| 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))
||.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 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
||.(X,seq,Cseq).|| is V11() V12() ext-real Element of REAL
Sum (||.seq.||,Cseq) is V11() V12() ext-real Element of REAL
||.((Partial_Sums seq) . Cseq).|| is V11() V12() ext-real Element of REAL
Partial_Sums ||.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))
(Partial_Sums ||.seq.||) . Cseq 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))
||.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))
Partial_Sums ||.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 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
(Partial_Sums ||.seq.||) . 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
(Partial_Sums seq) . n is Element of the U1 of X
((Partial_Sums seq) . n) - ((Partial_Sums seq) . Cseq) is Element of the U1 of X
- ((Partial_Sums seq) . Cseq) is Element of the U1 of X
K298(X,((Partial_Sums seq) . n),(- ((Partial_Sums seq) . Cseq))) is Element of the U1 of X
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . Cseq)).|| is V11() V12() ext-real Element of REAL
(Partial_Sums ||.seq.||) . n is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . Cseq) is V11() V12() ext-real Element of REAL
abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . 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
n + n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(n + n) + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
seq . ((n + n) + 1) is Element of the U1 of X
||.(seq . ((n + n) + 1)).|| is V11() V12() ext-real Element of REAL
n + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + (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 + (n + 1)) is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . (n + (n + 1))) is V11() V12() ext-real Element of REAL
abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . (n + (n + 1)))) is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . (n + (n + 1))) - ((Partial_Sums ||.seq.||) . n) is V11() V12() ext-real Element of REAL
- (((Partial_Sums ||.seq.||) . (n + (n + 1))) - ((Partial_Sums ||.seq.||) . n)) is V11() V12() ext-real Element of REAL
abs (- (((Partial_Sums ||.seq.||) . (n + (n + 1))) - ((Partial_Sums ||.seq.||) . n))) is V11() V12() ext-real Element of REAL
(Partial_Sums ||.seq.||) . ((n + n) + 1) is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . ((n + n) + 1)) - ((Partial_Sums ||.seq.||) . n) is V11() V12() ext-real Element of REAL
abs (((Partial_Sums ||.seq.||) . ((n + n) + 1)) - ((Partial_Sums ||.seq.||) . n)) is V11() V12() ext-real Element of REAL
(Partial_Sums ||.seq.||) . (n + n) is V11() V12() ext-real Element of REAL
||.seq.|| . ((n + n) + 1) is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . (n + n)) + (||.seq.|| . ((n + n) + 1)) is V11() V12() ext-real Element of REAL
(((Partial_Sums ||.seq.||) . (n + n)) + (||.seq.|| . ((n + n) + 1))) - ((Partial_Sums ||.seq.||) . n) is V11() V12() ext-real Element of REAL
abs ((((Partial_Sums ||.seq.||) . (n + n)) + (||.seq.|| . ((n + n) + 1))) - ((Partial_Sums ||.seq.||) . n)) is V11() V12() ext-real Element of REAL
||.(seq . ((n + n) + 1)).|| + ((Partial_Sums ||.seq.||) . (n + n)) is V11() V12() ext-real Element of REAL
(||.(seq . ((n + n) + 1)).|| + ((Partial_Sums ||.seq.||) . (n + n))) - ((Partial_Sums ||.seq.||) . n) is V11() V12() ext-real Element of REAL
abs ((||.(seq . ((n + n) + 1)).|| + ((Partial_Sums ||.seq.||) . (n + n))) - ((Partial_Sums ||.seq.||) . n)) is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . (n + n)) - ((Partial_Sums ||.seq.||) . n) is V11() V12() ext-real Element of REAL
(((Partial_Sums ||.seq.||) . (n + n)) - ((Partial_Sums ||.seq.||) . n)) + ||.(seq . ((n + n) + 1)).|| is V11() V12() ext-real Element of REAL
abs ((((Partial_Sums ||.seq.||) . (n + n)) - ((Partial_Sums ||.seq.||) . n)) + ||.(seq . ((n + n) + 1)).||) is V11() V12() ext-real Element of REAL
(Partial_Sums seq) . (n + (n + 1)) is Element of the U1 of X
((Partial_Sums seq) . n) - ((Partial_Sums seq) . (n + (n + 1))) is Element of the U1 of X
- ((Partial_Sums seq) . (n + (n + 1))) is Element of the U1 of X
K298(X,((Partial_Sums seq) . n),(- ((Partial_Sums seq) . (n + (n + 1))))) is Element of the U1 of X
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . (n + (n + 1)))).|| is V11() V12() ext-real Element of REAL
(Partial_Sums seq) . (n + n) is Element of the U1 of X
((Partial_Sums seq) . (n + n)) + (seq . ((n + n) + 1)) is Element of the U1 of X
((Partial_Sums seq) . n) - (((Partial_Sums seq) . (n + n)) + (seq . ((n + n) + 1))) is Element of the U1 of X
- (((Partial_Sums seq) . (n + n)) + (seq . ((n + n) + 1))) is Element of the U1 of X
K298(X,((Partial_Sums seq) . n),(- (((Partial_Sums seq) . (n + n)) + (seq . ((n + n) + 1))))) is Element of the U1 of X
||.(((Partial_Sums seq) . n) - (((Partial_Sums seq) . (n + n)) + (seq . ((n + n) + 1)))).|| is V11() V12() ext-real Element of REAL
((Partial_Sums seq) . n) - ((Partial_Sums seq) . (n + n)) is Element of the U1 of X
- ((Partial_Sums seq) . (n + n)) is Element of the U1 of X
K298(X,((Partial_Sums seq) . n),(- ((Partial_Sums seq) . (n + n)))) is Element of the U1 of X
(((Partial_Sums seq) . n) - ((Partial_Sums seq) . (n + n))) - (seq . ((n + n) + 1)) is Element of the U1 of X
- (seq . ((n + n) + 1)) is Element of the U1 of X
K298(X,(((Partial_Sums seq) . n) - ((Partial_Sums seq) . (n + n))),(- (seq . ((n + n) + 1)))) is Element of the U1 of X
||.((((Partial_Sums seq) . n) - ((Partial_Sums seq) . (n + n))) - (seq . ((n + n) + 1))).|| is V11() V12() ext-real Element of REAL
(((Partial_Sums seq) . n) - ((Partial_Sums seq) . (n + n))) + (- (seq . ((n + n) + 1))) is Element of the U1 of X
||.((((Partial_Sums seq) . n) - ((Partial_Sums seq) . (n + n))) + (- (seq . ((n + n) + 1)))).|| is V11() V12() ext-real Element of REAL
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . (n + n))).|| is V11() V12() ext-real Element of REAL
||.(- (seq . ((n + n) + 1))).|| is V11() V12() ext-real Element of REAL
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . (n + n))).|| + ||.(- (seq . ((n + n) + 1))).|| is V11() V12() ext-real Element of REAL
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . (n + n))).|| + ||.(seq . ((n + n) + 1)).|| is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . (n + n)) is V11() V12() ext-real Element of REAL
abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . (n + n))) is V11() V12() ext-real Element of REAL
(abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . (n + n)))) + ||.(seq . ((n + n) + 1)).|| is V11() V12() ext-real Element of REAL
- (((Partial_Sums ||.seq.||) . (n + n)) - ((Partial_Sums ||.seq.||) . n)) is V11() V12() ext-real Element of REAL
abs (- (((Partial_Sums ||.seq.||) . (n + n)) - ((Partial_Sums ||.seq.||) . n))) is V11() V12() ext-real Element of REAL
(abs (- (((Partial_Sums ||.seq.||) . (n + n)) - ((Partial_Sums ||.seq.||) . n)))) + ||.(seq . ((n + n) + 1)).|| is V11() V12() ext-real Element of REAL
abs (((Partial_Sums ||.seq.||) . (n + n)) - ((Partial_Sums ||.seq.||) . n)) is V11() V12() ext-real Element of REAL
(abs (((Partial_Sums ||.seq.||) . (n + n)) - ((Partial_Sums ||.seq.||) . n))) + ||.(seq . ((n + n) + 1)).|| is V11() V12() ext-real Element of REAL
k is V11() V12() ext-real integer set
k is V11() V12() ext-real integer set
k - k is V11() V12() ext-real integer set
n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + 0 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums seq) . (n + 0) is Element of the U1 of X
((Partial_Sums seq) . n) - ((Partial_Sums seq) . (n + 0)) is Element of the U1 of X
- ((Partial_Sums seq) . (n + 0)) is Element of the U1 of X
K298(X,((Partial_Sums seq) . n),(- ((Partial_Sums seq) . (n + 0)))) is Element of the U1 of X
||.(((Partial_Sums seq) . n) - ((Partial_Sums seq) . (n + 0))).|| is V11() V12() ext-real Element of REAL
0. X is V82(X) Element of the U1 of X
||.H₁(X).|| is V11() V12() ext-real Element of REAL
(Partial_Sums ||.seq.||) . (n + 0) is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . (n + 0)) is V11() V12() ext-real Element of REAL
abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . (n + 0))) 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
n + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Cseq + (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.||) . (Cseq + (n + 1)) is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . (Cseq + (n + 1))) - ((Partial_Sums ||.seq.||) . Cseq) is V11() V12() ext-real Element of REAL
abs (((Partial_Sums ||.seq.||) . (Cseq + (n + 1))) - ((Partial_Sums ||.seq.||) . Cseq)) is V11() V12() ext-real Element of REAL
Cseq + n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums ||.seq.||) . (Cseq + n) is V11() V12() ext-real Element of REAL
(Cseq + n) + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
||.seq.|| . ((Cseq + n) + 1) is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . (Cseq + n)) + (||.seq.|| . ((Cseq + n) + 1)) is V11() V12() ext-real Element of REAL
(((Partial_Sums ||.seq.||) . (Cseq + n)) + (||.seq.|| . ((Cseq + n) + 1))) - ((Partial_Sums ||.seq.||) . Cseq) is V11() V12() ext-real Element of REAL
abs ((((Partial_Sums ||.seq.||) . (Cseq + n)) + (||.seq.|| . ((Cseq + n) + 1))) - ((Partial_Sums ||.seq.||) . Cseq)) is V11() V12() ext-real Element of REAL
seq . ((Cseq + n) + 1) is Element of the U1 of X
||.(seq . ((Cseq + n) + 1)).|| is V11() V12() ext-real Element of REAL
||.(seq . ((Cseq + n) + 1)).|| + ((Partial_Sums ||.seq.||) . (Cseq + n)) is V11() V12() ext-real Element of REAL
(||.(seq . ((Cseq + n) + 1)).|| + ((Partial_Sums ||.seq.||) . (Cseq + n))) - ((Partial_Sums ||.seq.||) . Cseq) is V11() V12() ext-real Element of REAL
abs ((||.(seq . ((Cseq + n) + 1)).|| + ((Partial_Sums ||.seq.||) . (Cseq + n))) - ((Partial_Sums ||.seq.||) . Cseq)) is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . (Cseq + n)) - ((Partial_Sums ||.seq.||) . Cseq) is V11() V12() ext-real Element of REAL
||.(seq . ((Cseq + n) + 1)).|| + (((Partial_Sums ||.seq.||) . (Cseq + n)) - ((Partial_Sums ||.seq.||) . Cseq)) is V11() V12() ext-real Element of REAL
abs (||.(seq . ((Cseq + n) + 1)).|| + (((Partial_Sums ||.seq.||) . (Cseq + n)) - ((Partial_Sums ||.seq.||) . Cseq))) is V11() V12() ext-real Element of REAL
(Partial_Sums seq) . (Cseq + (n + 1)) is Element of the U1 of X
((Partial_Sums seq) . (Cseq + (n + 1))) - ((Partial_Sums seq) . Cseq) is Element of the U1 of X
K298(X,((Partial_Sums seq) . (Cseq + (n + 1))),(- ((Partial_Sums seq) . Cseq))) is Element of the U1 of X
||.(((Partial_Sums seq) . (Cseq + (n + 1))) - ((Partial_Sums seq) . Cseq)).|| is V11() V12() ext-real Element of REAL
(Partial_Sums seq) . (Cseq + n) is Element of the U1 of X
(seq . ((Cseq + n) + 1)) + ((Partial_Sums seq) . (Cseq + n)) is Element of the U1 of X
((seq . ((Cseq + n) + 1)) + ((Partial_Sums seq) . (Cseq + n))) - ((Partial_Sums seq) . Cseq) is Element of the U1 of X
K298(X,((seq . ((Cseq + n) + 1)) + ((Partial_Sums seq) . (Cseq + n))),(- ((Partial_Sums seq) . Cseq))) is Element of the U1 of X
||.(((seq . ((Cseq + n) + 1)) + ((Partial_Sums seq) . (Cseq + n))) - ((Partial_Sums seq) . Cseq)).|| is V11() V12() ext-real Element of REAL
((Partial_Sums seq) . (Cseq + n)) - ((Partial_Sums seq) . Cseq) is Element of the U1 of X
K298(X,((Partial_Sums seq) . (Cseq + n)),(- ((Partial_Sums seq) . Cseq))) is Element of the U1 of X
(seq . ((Cseq + n) + 1)) + (((Partial_Sums seq) . (Cseq + n)) - ((Partial_Sums seq) . Cseq)) is Element of the U1 of X
||.((seq . ((Cseq + n) + 1)) + (((Partial_Sums seq) . (Cseq + n)) - ((Partial_Sums seq) . Cseq))).|| is V11() V12() ext-real Element of REAL
||.(((Partial_Sums seq) . (Cseq + n)) - ((Partial_Sums seq) . Cseq)).|| is V11() V12() ext-real Element of REAL
||.(seq . ((Cseq + n) + 1)).|| + ||.(((Partial_Sums seq) . (Cseq + n)) - ((Partial_Sums seq) . Cseq)).|| is V11() V12() ext-real Element of REAL
abs (((Partial_Sums ||.seq.||) . (Cseq + n)) - ((Partial_Sums ||.seq.||) . Cseq)) is V11() V12() ext-real Element of REAL
||.(seq . ((Cseq + n) + 1)).|| + (abs (((Partial_Sums ||.seq.||) . (Cseq + n)) - ((Partial_Sums ||.seq.||) . Cseq))) is V11() V12() ext-real Element of REAL
k is V11() V12() ext-real integer set
k is V11() V12() ext-real integer set
k - k is V11() V12() ext-real integer set
n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Cseq + n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Cseq + 0 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums seq) . (Cseq + 0) is Element of the U1 of X
((Partial_Sums seq) . (Cseq + 0)) - ((Partial_Sums seq) . Cseq) is Element of the U1 of X
K298(X,((Partial_Sums seq) . (Cseq + 0)),(- ((Partial_Sums seq) . Cseq))) is Element of the U1 of X
||.(((Partial_Sums seq) . (Cseq + 0)) - ((Partial_Sums seq) . Cseq)).|| is V11() V12() ext-real Element of REAL
(Partial_Sums ||.seq.||) . (Cseq + 0) is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . (Cseq + 0)) - ((Partial_Sums ||.seq.||) . Cseq) is V11() V12() ext-real Element of REAL
abs (((Partial_Sums ||.seq.||) . (Cseq + 0)) - ((Partial_Sums ||.seq.||) . Cseq)) 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))
||.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 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
Sum (||.seq.||,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
(X,seq,n) is Element of the U1 of X
(Partial_Sums seq) . n is Element of the U1 of X
(X,seq,n) - (X,seq,Cseq) is Element of the U1 of X
- (X,seq,Cseq) is Element of the U1 of X
K298(X,(X,seq,n),(- (X,seq,Cseq))) is Element of the U1 of X
||.((X,seq,n) - (X,seq,Cseq)).|| is V11() V12() ext-real Element of REAL
Sum (||.seq.||,n) is V11() V12() ext-real Element of REAL
(Sum (||.seq.||,n)) - (Sum (||.seq.||,Cseq)) is V11() V12() ext-real Element of REAL
abs ((Sum (||.seq.||,n)) - (Sum (||.seq.||,Cseq))) is V11() V12() ext-real Element of REAL
(X,seq,n) - ((Partial_Sums seq) . Cseq) is Element of the U1 of X
- ((Partial_Sums seq) . Cseq) is Element of the U1 of X
K298(X,(X,seq,n),(- ((Partial_Sums seq) . Cseq))) is Element of the U1 of X
||.((X,seq,n) - ((Partial_Sums seq) . Cseq)).|| is V11() V12() ext-real Element of REAL
Partial_Sums ||.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))
(Partial_Sums ||.seq.||) . n is V11() V12() ext-real Element of REAL
(Partial_Sums ||.seq.||) . Cseq is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . Cseq) is V11() V12() ext-real Element of REAL
abs (((Partial_Sums ||.seq.||) . n) - ((Partial_Sums ||.seq.||) . Cseq)) is V11() V12() ext-real Element of REAL
(Sum (||.seq.||,n)) - ((Partial_Sums ||.seq.||) . Cseq) is V11() V12() ext-real Element of REAL
abs ((Sum (||.seq.||,n)) - ((Partial_Sums ||.seq.||) . Cseq)) 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))
||.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 V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,seq,n,Cseq) is Element of the U1 of X
(X,seq,n) 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) . n 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,n) - (X,seq,Cseq) is Element of the U1 of X
- (X,seq,Cseq) is Element of the U1 of X
K298(X,(X,seq,n),(- (X,seq,Cseq))) is Element of the U1 of X
||.(X,seq,n,Cseq).|| is V11() V12() ext-real Element of REAL
Sum (||.seq.||,n,Cseq) is V11() V12() ext-real Element of REAL
abs (Sum (||.seq.||,n,Cseq)) is V11() V12() ext-real Element of REAL
||.((X,seq,n) - (X,seq,Cseq)).|| is V11() V12() ext-real Element of REAL
Sum (||.seq.||,n) is V11() V12() ext-real Element of REAL
Sum (||.seq.||,Cseq) is V11() V12() ext-real Element of REAL
(Sum (||.seq.||,n)) - (Sum (||.seq.||,Cseq)) is V11() V12() ext-real Element of REAL
abs ((Sum (||.seq.||,n)) - (Sum (||.seq.||,Cseq))) 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))
||.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 V11() V12() ext-real Element of REAL
2 is V1() V4() V5() V6() V10() V11() V12() ext-real positive non negative integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Cseq / 2 is V11() V12() ext-real Element of REAL
Partial_Sums ||.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))
n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums ||.seq.||) . n 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))
m2 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums seq) . m2 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) . k is Element of the U1 of X
((Partial_Sums seq) . m2) - ((Partial_Sums seq) . k) is Element of the U1 of X
- ((Partial_Sums seq) . k) is Element of the U1 of X
K298(X,((Partial_Sums seq) . m2),(- ((Partial_Sums seq) . k))) is Element of the U1 of X
||.(((Partial_Sums seq) . m2) - ((Partial_Sums seq) . k)).|| is V11() V12() ext-real Element of REAL
(Partial_Sums ||.seq.||) . m2 is V11() V12() ext-real Element of REAL
(Partial_Sums ||.seq.||) . k is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . m2) - ((Partial_Sums ||.seq.||) . k) is V11() V12() ext-real Element of REAL
abs (((Partial_Sums ||.seq.||) . m2) - ((Partial_Sums ||.seq.||) . k)) is V11() V12() ext-real Element of REAL
k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums ||.seq.||) . k is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . k) - ((Partial_Sums ||.seq.||) . k) is V11() V12() ext-real Element of REAL
abs (((Partial_Sums ||.seq.||) . k) - ((Partial_Sums ||.seq.||) . k)) is V11() V12() ext-real Element of REAL
((Partial_Sums ||.seq.||) . m2) - ((Partial_Sums ||.seq.||) . k) is V11() V12() ext-real Element of REAL
abs (((Partial_Sums ||.seq.||) . m2) - ((Partial_Sums ||.seq.||) . k)) is V11() V12() ext-real Element of REAL
(Cseq / 2) + (Cseq / 2) is V11() V12() ext-real Element of REAL
(abs (((Partial_Sums ||.seq.||) . m2) - ((Partial_Sums ||.seq.||) . k))) + (abs (((Partial_Sums ||.seq.||) . k) - ((Partial_Sums ||.seq.||) . k))) is V11() V12() ext-real Element of REAL
(((Partial_Sums ||.seq.||) . m2) - ((Partial_Sums ||.seq.||) . k)) - (((Partial_Sums ||.seq.||) . k) - ((Partial_Sums ||.seq.||) . k)) is V11() V12() ext-real Element of REAL
abs ((((Partial_Sums ||.seq.||) . m2) - ((Partial_Sums ||.seq.||) . k)) - (((Partial_Sums ||.seq.||) . k) - ((Partial_Sums ||.seq.||) . k))) is V11() V12() ext-real Element of REAL
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
(Partial_Sums seq) . k is Element of the U1 of X
(Partial_Sums seq) . m2 is Element of the U1 of X
((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 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( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
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 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 . k is Element of the U1 of X
Cseq . k is V11() Element of COMPLEX
(Cseq . k) * (seq . k) is Element of the U1 of X
k . k 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 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))
n is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
(X,(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))
(X,seq,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,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))
(X,seq,n) + (X,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
(X,(seq + Cseq),n) . k is Element of the U1 of X
(seq + Cseq) . k is Element of the U1 of X
n . k is V11() Element of COMPLEX
(n . k) * ((seq + Cseq) . k) is Element of the U1 of X
seq . k is Element of the U1 of X
Cseq . k is Element of the U1 of X
(seq . k) + (Cseq . k) is Element of the U1 of X
(n . k) * ((seq . k) + (Cseq . k)) is Element of the U1 of X
(n . k) * (seq . k) is Element of the U1 of X
(n . k) * (Cseq . k) is Element of the U1 of X
((n . k) * (seq . k)) + ((n . k) * (Cseq . k)) is Element of the U1 of X
(X,seq,n) . k is Element of the U1 of X
((X,seq,n) . k) + ((n . k) * (Cseq . k)) is Element of the U1 of X
(X,Cseq,n) . k is Element of the U1 of X
((X,seq,n) . k) + ((X,Cseq,n) . k) is Element of the U1 of X
((X,seq,n) + (X,Cseq,n)) . k 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 V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
(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))
n is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
Cseq + n is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
(X,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))
(X,seq,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,seq,Cseq) + (X,seq,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
(X,seq,(Cseq + n)) . k is Element of the U1 of X
seq . k is Element of the U1 of X
(Cseq + n) . k is V11() Element of COMPLEX
((Cseq + n) . k) * (seq . k) is Element of the U1 of X
Cseq . k is V11() Element of COMPLEX
n . k is V11() Element of COMPLEX
(Cseq . k) + (n . k) is V11() Element of COMPLEX
((Cseq . k) + (n . k)) * (seq . k) is Element of the U1 of X
(Cseq . k) * (seq . k) is Element of the U1 of X
(n . k) * (seq . k) is Element of the U1 of X
((Cseq . k) * (seq . k)) + ((n . k) * (seq . k)) is Element of the U1 of X
(X,seq,Cseq) . k is Element of the U1 of X
((X,seq,Cseq) . k) + ((n . k) * (seq . k)) is Element of the U1 of X
(X,seq,n) . k is Element of the U1 of X
((X,seq,Cseq) . k) + ((X,seq,n) . k) is Element of the U1 of X
((X,seq,Cseq) + (X,seq,n)) . k 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 V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
n is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
Cseq (#) n is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
(X,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))
(X,seq,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,(X,seq,n),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
(X,seq,(Cseq (#) n)) . k is Element of the U1 of X
seq . k is Element of the U1 of X
(Cseq (#) n) . k is V11() Element of COMPLEX
((Cseq (#) n) . k) * (seq . k) is Element of the U1 of X
Cseq . k is V11() Element of COMPLEX
n . k is V11() Element of COMPLEX
(Cseq . k) * (n . k) is V11() Element of COMPLEX
((Cseq . k) * (n . k)) * (seq . k) is Element of the U1 of X
(n . k) * (seq . k) is Element of the U1 of X
(Cseq . k) * ((n . k) * (seq . k)) is Element of the U1 of X
(X,seq,n) . k is Element of the U1 of X
(Cseq . k) * ((X,seq,n) . k) is Element of the U1 of X
(X,(X,seq,n),Cseq) . k 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 V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
(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))
n is V11() set
n (#) Cseq is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
(X,seq,(n (#) 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 * (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))
k is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,seq,(n (#) Cseq)) . k is Element of the U1 of X
seq . k is Element of the U1 of X
(n (#) Cseq) . k is V11() Element of COMPLEX
((n (#) Cseq) . k) * (seq . k) is Element of the U1 of X
Cseq . k is V11() Element of COMPLEX
n * (Cseq . k) is V11() set
(n * (Cseq . k)) * (seq . k) is Element of the U1 of X
(Cseq . k) * (seq . k) is Element of the U1 of X
n * ((Cseq . k) * (seq . k)) is Element of the U1 of X
(X,seq,Cseq) . k is Element of the U1 of X
n * ((X,seq,Cseq) . k) is Element of the U1 of X
(n * (X,seq,Cseq)) . k 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))
Cseq is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
(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))
- Cseq is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
- 1 is V1() V11() V12() ext-real non positive negative integer set
(- 1) (#) Cseq is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
(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))
n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,(- seq),Cseq) . n is Element of the U1 of X
(- seq) . n is Element of the U1 of X
Cseq . n is V11() Element of COMPLEX
(Cseq . n) * ((- seq) . n) is Element of the U1 of X
seq . n is Element of the U1 of X
- (seq . n) is Element of the U1 of X
(Cseq . n) * (- (seq . n)) is Element of the U1 of X
- (Cseq . n) is V11() Element of COMPLEX
(- (Cseq . n)) * (seq . n) is Element of the U1 of X
(- Cseq) . n is V11() Element of COMPLEX
((- Cseq) . n) * (seq . n) is Element of the U1 of X
(X,seq,(- Cseq)) . 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))
Cseq is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
(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))
n is V11() Element of COMPLEX
k is Element of the U1 of X
n * k is Element of the U1 of X
m is V11() V12() ext-real Element of REAL
||.k.|| is V11() V12() ext-real Element of REAL
m + ||.k.|| is V11() V12() ext-real Element of REAL
0 + 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
m2 is V11() V12() ext-real Element of REAL
m2 / (m + ||.k.||) 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
m2 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n + m2 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
m is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Cseq . n is V11() Element of COMPLEX
(Cseq . n) - n is V11() Element of COMPLEX
|.((Cseq . n) - n).| is V11() V12() ext-real Element of REAL
||.k.|| * |.((Cseq . n) - n).| is V11() V12() ext-real Element of REAL
||.k.|| * (m2 / (m + ||.k.||)) is V11() V12() ext-real Element of REAL
|.(Cseq . n).| is V11() V12() ext-real Element of REAL
seq . n is Element of the U1 of X
(seq . n) - k is Element of the U1 of X
- k is Element of the U1 of X
K298(X,(seq . n),(- k)) is Element of the U1 of X
||.((seq . n) - k).|| is V11() V12() ext-real Element of REAL
m * (m2 / (m + ||.k.||)) is V11() V12() ext-real Element of REAL
|.(Cseq . n).| * ||.((seq . n) - k).|| is V11() V12() ext-real Element of REAL
(m * (m2 / (m + ||.k.||))) + (||.k.|| * (m2 / (m + ||.k.||))) is V11() V12() ext-real Element of REAL
(|.(Cseq . n).| * ||.((seq . n) - k).||) + (||.k.|| * |.((Cseq . n) - n).|) is V11() V12() ext-real Element of REAL
m * m2 is V11() V12() ext-real Element of REAL
(m * m2) / (m + ||.k.||) is V11() V12() ext-real Element of REAL
((m * m2) / (m + ||.k.||)) + (||.k.|| * (m2 / (m + ||.k.||))) is V11() V12() ext-real Element of REAL
||.k.|| * m2 is V11() V12() ext-real Element of REAL
(||.k.|| * m2) / (m + ||.k.||) is V11() V12() ext-real Element of REAL
((m * m2) / (m + ||.k.||)) + ((||.k.|| * m2) / (m + ||.k.||)) is V11() V12() ext-real Element of REAL
(m * m2) + (||.k.|| * m2) is V11() V12() ext-real Element of REAL
((m * m2) + (||.k.|| * m2)) / (m + ||.k.||) is V11() V12() ext-real Element of REAL
(m + ||.k.||) * m2 is V11() V12() ext-real Element of REAL
((m + ||.k.||) * m2) / (m + ||.k.||) is V11() V12() ext-real Element of REAL
(X,seq,Cseq) . n is Element of the U1 of X
((X,seq,Cseq) . n) - (n * k) is Element of the U1 of X
- (n * k) is Element of the U1 of X
K298(X,((X,seq,Cseq) . n),(- (n * k))) is Element of the U1 of X
||.(((X,seq,Cseq) . n) - (n * k)).|| is V11() V12() ext-real Element of REAL
(Cseq . n) * (seq . n) is Element of the U1 of X
((Cseq . n) * (seq . n)) - (n * k) is Element of the U1 of X
K298(X,((Cseq . n) * (seq . n)),(- (n * k))) is Element of the U1 of X
||.(((Cseq . n) * (seq . n)) - (n * k)).|| is V11() V12() ext-real Element of REAL
0. X is V82(X) Element of the U1 of X
(((Cseq . n) * (seq . n)) - (n * k)) + H₁(X) is Element of the U1 of X
||.((((Cseq . n) * (seq . n)) - (n * k)) + H₁(X)).|| is V11() V12() ext-real Element of REAL
(Cseq . n) * k is Element of the U1 of X
((Cseq . n) * k) - ((Cseq . n) * k) is Element of the U1 of X
- ((Cseq . n) * k) is Element of the U1 of X
K298(X,((Cseq . n) * k),(- ((Cseq . n) * k))) is Element of the U1 of X
(((Cseq . n) * (seq . n)) - (n * k)) + (((Cseq . n) * k) - ((Cseq . n) * k)) is Element of the U1 of X
||.((((Cseq . n) * (seq . n)) - (n * k)) + (((Cseq . n) * k) - ((Cseq . n) * k))).|| is V11() V12() ext-real Element of REAL
(n * k) - (((Cseq . n) * k) - ((Cseq . n) * k)) is Element of the U1 of X
- (((Cseq . n) * k) - ((Cseq . n) * k)) is Element of the U1 of X
K298(X,(n * k),(- (((Cseq . n) * k) - ((Cseq . n) * k)))) is Element of the U1 of X
((Cseq . n) * (seq . n)) - ((n * k) - (((Cseq . n) * k) - ((Cseq . n) * k))) is Element of the U1 of X
- ((n * k) - (((Cseq . n) * k) - ((Cseq . n) * k))) is Element of the U1 of X
K298(X,((Cseq . n) * (seq . n)),(- ((n * k) - (((Cseq . n) * k) - ((Cseq . n) * k))))) is Element of the U1 of X
||.(((Cseq . n) * (seq . n)) - ((n * k) - (((Cseq . n) * k) - ((Cseq . n) * k)))).|| is V11() V12() ext-real Element of REAL
(n * k) - ((Cseq . n) * k) is Element of the U1 of X
K298(X,(n * k),(- ((Cseq . n) * k))) is Element of the U1 of X
((Cseq . n) * k) + ((n * k) - ((Cseq . n) * k)) is Element of the U1 of X
((Cseq . n) * (seq . n)) - (((Cseq . n) * k) + ((n * k) - ((Cseq . n) * k))) is Element of the U1 of X
- (((Cseq . n) * k) + ((n * k) - ((Cseq . n) * k))) is Element of the U1 of X
K298(X,((Cseq . n) * (seq . n)),(- (((Cseq . n) * k) + ((n * k) - ((Cseq . n) * k))))) is Element of the U1 of X
||.(((Cseq . n) * (seq . n)) - (((Cseq . n) * k) + ((n * k) - ((Cseq . n) * k)))).|| is V11() V12() ext-real Element of REAL
((Cseq . n) * (seq . n)) - ((Cseq . n) * k) is Element of the U1 of X
K298(X,((Cseq . n) * (seq . n)),(- ((Cseq . n) * k))) is Element of the U1 of X
(((Cseq . n) * (seq . n)) - ((Cseq . n) * k)) - ((n * k) - ((Cseq . n) * k)) is Element of the U1 of X
- ((n * k) - ((Cseq . n) * k)) is Element of the U1 of X
K298(X,(((Cseq . n) * (seq . n)) - ((Cseq . n) * k)),(- ((n * k) - ((Cseq . n) * k)))) is Element of the U1 of X
||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * k)) - ((n * k) - ((Cseq . n) * k))).|| is V11() V12() ext-real Element of REAL
((Cseq . n) * k) - (n * k) is Element of the U1 of X
K298(X,((Cseq . n) * k),(- (n * k))) is Element of the U1 of X
(((Cseq . n) * (seq . n)) - ((Cseq . n) * k)) + (((Cseq . n) * k) - (n * k)) is Element of the U1 of X
||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * k)) + (((Cseq . n) * k) - (n * k))).|| is V11() V12() ext-real Element of REAL
||.(((Cseq . n) * (seq . n)) - ((Cseq . n) * k)).|| is V11() V12() ext-real Element of REAL
||.(((Cseq . n) * k) - (n * k)).|| is V11() V12() ext-real Element of REAL
||.(((Cseq . n) * (seq . n)) - ((Cseq . n) * k)).|| + ||.(((Cseq . n) * k) - (n * k)).|| is V11() V12() ext-real Element of REAL
(Cseq . n) * ((seq . n) - k) is Element of the U1 of X
||.((Cseq . n) * ((seq . n) - k)).|| is V11() V12() ext-real Element of REAL
||.((Cseq . n) * ((seq . n) - k)).|| + ||.(((Cseq . n) * k) - (n * k)).|| is V11() V12() ext-real Element of REAL
((Cseq . n) - n) * k is Element of the U1 of X
||.(((Cseq . n) - n) * k).|| is V11() V12() ext-real Element of REAL
||.((Cseq . n) * ((seq . n) - k)).|| + ||.(((Cseq . n) - n) * k).|| is V11() V12() ext-real Element of REAL
(|.(Cseq . n).| * ||.((seq . n) - k).||) + ||.(((Cseq . n) - n) * k).|| is V11() V12() ext-real Element of REAL
k is Element of the U1 of X
((X,seq,Cseq) . n) - k is Element of the U1 of X
- k is Element of the U1 of X
K298(X,((X,seq,Cseq) . n),(- k)) is Element of the U1 of X
||.(((X,seq,Cseq) . n) - k).|| is V11() V12() ext-real Element of REAL
k 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 V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
(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))
n is V11() V12() ext-real Element of REAL
k is V11() V12() ext-real Element of REAL
n * k is V11() V12() ext-real Element of REAL
m is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Cseq . m is V11() Element of COMPLEX
|.(Cseq . m).| is V11() V12() ext-real Element of REAL
seq . m is Element of the U1 of X
||.(seq . m).|| is V11() V12() ext-real Element of REAL
|.(Cseq . m).| * ||.(seq . m).|| is V11() V12() ext-real Element of REAL
|.(Cseq . m).| * k is V11() V12() ext-real Element of REAL
(X,seq,Cseq) . m is Element of the U1 of X
||.((X,seq,Cseq) . m).|| is V11() V12() ext-real Element of REAL
(Cseq . m) * (seq . m) is Element of the U1 of X
||.((Cseq . m) * (seq . m)).|| is V11() V12() ext-real Element of REAL
m2 is V11() V12() ext-real Element of REAL
m is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(X,seq,Cseq) . m is Element of the U1 of X
||.((X,seq,Cseq) . m).|| is V11() V12() ext-real Element of REAL
k 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))
lim seq is Element of the U1 of X
Cseq is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
(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))
lim (X,seq,Cseq) is Element of the U1 of X
lim Cseq is V11() Element of COMPLEX
(lim Cseq) * (lim seq) is Element of the U1 of X
n is V11() V12() ext-real Element of REAL
||.(lim seq).|| is V11() V12() ext-real Element of REAL
n + ||.(lim seq).|| is V11() V12() ext-real Element of REAL
0 + 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
k is V11() V12() ext-real Element of REAL
k / (n + ||.(lim seq).||) is V11() V12() ext-real Element of REAL
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
k + m2 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
m is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
n is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
Cseq . n is V11() Element of COMPLEX
(Cseq . n) - (lim Cseq) is V11() Element of COMPLEX
|.((Cseq . n) - (lim Cseq)).| is V11() V12() ext-real Element of REAL
||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).| is V11() V12() ext-real Element of REAL
||.(lim seq).|| * (k / (n + ||.(lim seq).||)) is V11() V12() ext-real Element of REAL
seq . n is Element of the U1 of X
(seq . n) - (lim seq) is Element of the U1 of X
- (lim seq) is Element of the U1 of X
K298(X,(seq . n),(- (lim seq))) is Element of the U1 of X
||.((seq . n) - (lim seq)).|| is V11() V12() ext-real Element of REAL
dist ((seq . n),(lim seq)) is V11() V12() ext-real Element of REAL
|.(Cseq . n).| is V11() V12() ext-real Element of REAL
n * (k / (n + ||.(lim seq).||)) is V11() V12() ext-real Element of REAL
|.(Cseq . n).| * ||.((seq . n) - (lim seq)).|| is V11() V12() ext-real Element of REAL
(n * (k / (n + ||.(lim seq).||))) + (||.(lim seq).|| * (k / (n + ||.(lim seq).||))) is V11() V12() ext-real Element of REAL
(|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) is V11() V12() ext-real Element of REAL
n * k is V11() V12() ext-real Element of REAL
(n * k) / (n + ||.(lim seq).||) is V11() V12() ext-real Element of REAL
((n * k) / (n + ||.(lim seq).||)) + (||.(lim seq).|| * (k / (n + ||.(lim seq).||))) is V11() V12() ext-real Element of REAL
||.(lim seq).|| * k is V11() V12() ext-real Element of REAL
(||.(lim seq).|| * k) / (n + ||.(lim seq).||) is V11() V12() ext-real Element of REAL
((n * k) / (n + ||.(lim seq).||)) + ((||.(lim seq).|| * k) / (n + ||.(lim seq).||)) is V11() V12() ext-real Element of REAL
(n * k) + (||.(lim seq).|| * k) is V11() V12() ext-real Element of REAL
((n * k) + (||.(lim seq).|| * k)) / (n + ||.(lim seq).||) is V11() V12() ext-real Element of REAL
(n + ||.(lim seq).||) * k is V11() V12() ext-real Element of REAL
((n + ||.(lim seq).||) * k) / (n + ||.(lim seq).||) is V11() V12() ext-real Element of REAL
(X,seq,Cseq) . n is Element of the U1 of X
((X,seq,Cseq) . n) - ((lim Cseq) * (lim seq)) is Element of the U1 of X
- ((lim Cseq) * (lim seq)) is Element of the U1 of X
K298(X,((X,seq,Cseq) . n),(- ((lim Cseq) * (lim seq)))) is Element of the U1 of X
||.(((X,seq,Cseq) . n) - ((lim Cseq) * (lim seq))).|| is V11() V12() ext-real Element of REAL
(Cseq . n) * (seq . n) is Element of the U1 of X
((Cseq . n) * (seq . n)) - ((lim Cseq) * (lim seq)) is Element of the U1 of X
K298(X,((Cseq . n) * (seq . n)),(- ((lim Cseq) * (lim seq)))) is Element of the U1 of X
||.(((Cseq . n) * (seq . n)) - ((lim Cseq) * (lim seq))).|| is V11() V12() ext-real Element of REAL
0. X is V82(X) Element of the U1 of X
(((Cseq . n) * (seq . n)) - ((lim Cseq) * (lim seq))) + H₁(X) is Element of the U1 of X
||.((((Cseq . n) * (seq . n)) - ((lim Cseq) * (lim seq))) + H₁(X)).|| is V11() V12() ext-real Element of REAL
(Cseq . n) * (lim seq) is Element of the U1 of X
((Cseq . n) * (lim seq)) - ((Cseq . n) * (lim seq)) is Element of the U1 of X
- ((Cseq . n) * (lim seq)) is Element of the U1 of X
K298(X,((Cseq . n) * (lim seq)),(- ((Cseq . n) * (lim seq)))) is Element of the U1 of X
(((Cseq . n) * (seq . n)) - ((lim Cseq) * (lim seq))) + (((Cseq . n) * (lim seq)) - ((Cseq . n) * (lim seq))) is Element of the U1 of X
||.((((Cseq . n) * (seq . n)) - ((lim Cseq) * (lim seq))) + (((Cseq . n) * (lim seq)) - ((Cseq . n) * (lim seq)))).|| is V11() V12() ext-real Element of REAL
((lim Cseq) * (lim seq)) - (((Cseq . n) * (lim seq)) - ((Cseq . n) * (lim seq))) is Element of the U1 of X
- (((Cseq . n) * (lim seq)) - ((Cseq . n) * (lim seq))) is Element of the U1 of X
K298(X,((lim Cseq) * (lim seq)),(- (((Cseq . n) * (lim seq)) - ((Cseq . n) * (lim seq))))) is Element of the U1 of X
((Cseq . n) * (seq . n)) - (((lim Cseq) * (lim seq)) - (((Cseq . n) * (lim seq)) - ((Cseq . n) * (lim seq)))) is Element of the U1 of X
- (((lim Cseq) * (lim seq)) - (((Cseq . n) * (lim seq)) - ((Cseq . n) * (lim seq)))) is Element of the U1 of X
K298(X,((Cseq . n) * (seq . n)),(- (((lim Cseq) * (lim seq)) - (((Cseq . n) * (lim seq)) - ((Cseq . n) * (lim seq)))))) is Element of the U1 of X
||.(((Cseq . n) * (seq . n)) - (((lim Cseq) * (lim seq)) - (((Cseq . n) * (lim seq)) - ((Cseq . n) * (lim seq))))).|| is V11() V12() ext-real Element of REAL
((lim Cseq) * (lim seq)) - ((Cseq . n) * (lim seq)) is Element of the U1 of X
K298(X,((lim Cseq) * (lim seq)),(- ((Cseq . n) * (lim seq)))) is Element of the U1 of X
((Cseq . n) * (lim seq)) + (((lim Cseq) * (lim seq)) - ((Cseq . n) * (lim seq))) is Element of the U1 of X
((Cseq . n) * (seq . n)) - (((Cseq . n) * (lim seq)) + (((lim Cseq) * (lim seq)) - ((Cseq . n) * (lim seq)))) is Element of the U1 of X
- (((Cseq . n) * (lim seq)) + (((lim Cseq) * (lim seq)) - ((Cseq . n) * (lim seq)))) is Element of the U1 of X
K298(X,((Cseq . n) * (seq . n)),(- (((Cseq . n) * (lim seq)) + (((lim Cseq) * (lim seq)) - ((Cseq . n) * (lim seq)))))) is Element of the U1 of X
||.(((Cseq . n) * (seq . n)) - (((Cseq . n) * (lim seq)) + (((lim Cseq) * (lim seq)) - ((Cseq . n) * (lim seq))))).|| is V11() V12() ext-real Element of REAL
((Cseq . n) * (seq . n)) - ((Cseq . n) * (lim seq)) is Element of the U1 of X
K298(X,((Cseq . n) * (seq . n)),(- ((Cseq . n) * (lim seq)))) is Element of the U1 of X
(((Cseq . n) * (seq . n)) - ((Cseq . n) * (lim seq))) - (((lim Cseq) * (lim seq)) - ((Cseq . n) * (lim seq))) is Element of the U1 of X
- (((lim Cseq) * (lim seq)) - ((Cseq . n) * (lim seq))) is Element of the U1 of X
K298(X,(((Cseq . n) * (seq . n)) - ((Cseq . n) * (lim seq))),(- (((lim Cseq) * (lim seq)) - ((Cseq . n) * (lim seq))))) is Element of the U1 of X
||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * (lim seq))) - (((lim Cseq) * (lim seq)) - ((Cseq . n) * (lim seq)))).|| is V11() V12() ext-real Element of REAL
((Cseq . n) * (lim seq)) - ((lim Cseq) * (lim seq)) is Element of the U1 of X
K298(X,((Cseq . n) * (lim seq)),(- ((lim Cseq) * (lim seq)))) is Element of the U1 of X
(((Cseq . n) * (seq . n)) - ((Cseq . n) * (lim seq))) + (((Cseq . n) * (lim seq)) - ((lim Cseq) * (lim seq))) is Element of the U1 of X
||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * (lim seq))) + (((Cseq . n) * (lim seq)) - ((lim Cseq) * (lim seq)))).|| is V11() V12() ext-real Element of REAL
||.(((Cseq . n) * (seq . n)) - ((Cseq . n) * (lim seq))).|| is V11() V12() ext-real Element of REAL
||.(((Cseq . n) * (lim seq)) - ((lim Cseq) * (lim seq))).|| is V11() V12() ext-real Element of REAL
||.(((Cseq . n) * (seq . n)) - ((Cseq . n) * (lim seq))).|| + ||.(((Cseq . n) * (lim seq)) - ((lim Cseq) * (lim seq))).|| is V11() V12() ext-real Element of REAL
(Cseq . n) * ((seq . n) - (lim seq)) is Element of the U1 of X
||.((Cseq . n) * ((seq . n) - (lim seq))).|| is V11() V12() ext-real Element of REAL
||.((Cseq . n) * ((seq . n) - (lim seq))).|| + ||.(((Cseq . n) * (lim seq)) - ((lim Cseq) * (lim seq))).|| is V11() V12() ext-real Element of REAL
((Cseq . n) - (lim Cseq)) * (lim seq) is Element of the U1 of X
||.(((Cseq . n) - (lim Cseq)) * (lim seq)).|| is V11() V12() ext-real Element of REAL
||.((Cseq . n) * ((seq . n) - (lim seq))).|| + ||.(((Cseq . n) - (lim Cseq)) * (lim seq)).|| is V11() V12() ext-real Element of REAL
(|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + ||.(((Cseq . n) - (lim Cseq)) * (lim seq)).|| is V11() V12() ext-real Element of REAL
dist (((X,seq,Cseq) . n),((lim Cseq) * (lim seq))) 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))
seq is V75() V101() V126() V127() V128() V147() V148() V149() V150() ComplexUnitarySpace-like V160() CUNITSTR
the U1 of seq is V1() set
K7(NAT, the U1 of seq) is set
K6(K7(NAT, the U1 of seq)) is set
Cseq is V1() V13() V16( NAT ) V17( the U1 of seq) V18() V23( NAT ) V27( NAT , the U1 of seq) Element of K6(K7(NAT, the U1 of seq))
(seq,Cseq,X) is V1() V13() V16( NAT ) V17( the U1 of seq) V18() V23( NAT ) V27( NAT , the U1 of seq) Element of K6(K7(NAT, the U1 of seq))
n is V11() V12() ext-real Element of REAL
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
X . k is V11() Element of COMPLEX
m2 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
X . m2 is V11() Element of COMPLEX
(X . m2) - (X . k) is V11() Element of COMPLEX
|.((X . m2) - (X . k)).| 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))
Cseq is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
Cseq ^\ 1 is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued subsequence of Cseq
Cseq - (Cseq ^\ 1) is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
- (Cseq ^\ 1) is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
- 1 is V1() V11() V12() ext-real non positive negative integer set
(- 1) (#) (Cseq ^\ 1) is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
Cseq + (- (Cseq ^\ 1)) is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
(X,(Partial_Sums seq),(Cseq - (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 (X,(Partial_Sums seq),(Cseq - (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))
(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 (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,(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 (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . 0 is Element of the U1 of X
(X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1))) . 0 is Element of the U1 of X
(Partial_Sums seq) . 0 is Element of the U1 of X
(Cseq - (Cseq ^\ 1)) . 0 is V11() Element of COMPLEX
((Cseq - (Cseq ^\ 1)) . 0) * ((Partial_Sums seq) . 0) is Element of the U1 of X
seq . 0 is Element of the U1 of X
- (Cseq ^\ 1) is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
Cseq + (- (Cseq ^\ 1)) is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
(Cseq + (- (Cseq ^\ 1))) . 0 is V11() Element of COMPLEX
((Cseq + (- (Cseq ^\ 1))) . 0) * (seq . 0) is Element of the U1 of X
Cseq . 0 is V11() Element of COMPLEX
(- (Cseq ^\ 1)) . 0 is V11() Element of COMPLEX
(Cseq . 0) + ((- (Cseq ^\ 1)) . 0) is V11() Element of COMPLEX
((Cseq . 0) + ((- (Cseq ^\ 1)) . 0)) * (seq . 0) is Element of the U1 of X
(Cseq ^\ 1) . 0 is V11() Element of COMPLEX
- ((Cseq ^\ 1) . 0) is V11() Element of COMPLEX
(Cseq . 0) + (- ((Cseq ^\ 1) . 0)) is V11() Element of COMPLEX
((Cseq . 0) + (- ((Cseq ^\ 1) . 0))) * (seq . 0) is Element of the U1 of X
(Cseq . 0) - ((Cseq ^\ 1) . 0) is V11() Element of COMPLEX
((Cseq . 0) - ((Cseq ^\ 1) . 0)) * (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
Cseq . (0 + 1) is V11() Element of COMPLEX
(Cseq . 0) - (Cseq . (0 + 1)) is V11() Element of COMPLEX
((Cseq . 0) - (Cseq . (0 + 1))) * (seq . 0) is Element of the U1 of X
(Cseq . 0) * (seq . 0) is Element of the U1 of X
Cseq . 1 is V11() Element of COMPLEX
(Cseq . 1) * (seq . 0) is Element of the U1 of X
((Cseq . 0) * (seq . 0)) - ((Cseq . 1) * (seq . 0)) is Element of the U1 of X
- ((Cseq . 1) * (seq . 0)) is Element of the U1 of X
K298(X,((Cseq . 0) * (seq . 0)),(- ((Cseq . 1) * (seq . 0)))) is Element of the U1 of X
(X,(Partial_Sums seq),Cseq) . (0 + 1) is Element of the U1 of X
(Partial_Sums seq) . (0 + 1) is Element of the U1 of X
(Cseq . (0 + 1)) * ((Partial_Sums seq) . (0 + 1)) is Element of the U1 of X
seq . (0 + 1) is Element of the U1 of X
((Partial_Sums seq) . 0) + (seq . (0 + 1)) is Element of the U1 of X
(Cseq . (0 + 1)) * (((Partial_Sums seq) . 0) + (seq . (0 + 1))) 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
(Cseq . 1) * ((seq . 0) + (seq . 1)) is Element of the U1 of X
(Cseq . 1) * (seq . 1) is Element of the U1 of X
((Cseq . 1) * (seq . 0)) + ((Cseq . 1) * (seq . 1)) 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
(Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n is Element of the U1 of X
n + 1 is V4() V5() V6() V10() V11() V12() ext-real integer V58() V59() V60() V61() V62() V63() V64() Element of NAT
(Partial_Sums (X,seq,Cseq)) . (n + 1) is Element of the U1 of X
(X,(Partial_Sums seq),Cseq) . (n + 1) is Element of the U1 of X
((Partial_Sums (X,seq,Cseq)) . (n + 1)) - ((X,(Partial_Sums seq),Cseq) . (n + 1)) is Element of the U1 of X
- ((X,(Partial_Sums seq),Cseq) . (n + 1)) is Element of the U1 of X
K298(X,((Partial_Sums (X,seq,Cseq)) . (n + 1)),(- ((X,(Partial_Sums seq),Cseq) . (n + 1)))) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n) + ((X,(Partial_Sums seq),Cseq) . (n + 1)) is Element of the U1 of X
((X,(Partial_Sums seq),Cseq) . (n + 1)) - ((X,(Partial_Sums seq),Cseq) . (n + 1)) is Element of the U1 of X
K298(X,((X,(Partial_Sums seq),Cseq) . (n + 1)),(- ((X,(Partial_Sums seq),Cseq) . (n + 1)))) is Element of the U1 of X
((Partial_Sums (X,seq,Cseq)) . (n + 1)) - (((X,(Partial_Sums seq),Cseq) . (n + 1)) - ((X,(Partial_Sums seq),Cseq) . (n + 1))) is Element of the U1 of X
- (((X,(Partial_Sums seq),Cseq) . (n + 1)) - ((X,(Partial_Sums seq),Cseq) . (n + 1))) is Element of the U1 of X
K298(X,((Partial_Sums (X,seq,Cseq)) . (n + 1)),(- (((X,(Partial_Sums seq),Cseq) . (n + 1)) - ((X,(Partial_Sums seq),Cseq) . (n + 1))))) is Element of the U1 of X
0. X is V82(X) Element of the U1 of X
((Partial_Sums (X,seq,Cseq)) . (n + 1)) - H₁(X) is Element of the U1 of X
- (0. X) is Element of the U1 of X
K298(X,((Partial_Sums (X,seq,Cseq)) . (n + 1)),(- (0. X))) 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 (X,seq,Cseq)) . ((n + 1) + 1) is Element of the U1 of X
(X,seq,Cseq) . ((n + 1) + 1) is Element of the U1 of X
((Partial_Sums (X,seq,Cseq)) . (n + 1)) + ((X,seq,Cseq) . ((n + 1) + 1)) is Element of the U1 of X
(((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n) + ((X,(Partial_Sums seq),Cseq) . (n + 1))) + ((X,seq,Cseq) . ((n + 1) + 1)) is Element of the U1 of X
((X,(Partial_Sums seq),Cseq) . (n + 1)) + ((X,seq,Cseq) . ((n + 1) + 1)) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n) + (((X,(Partial_Sums seq),Cseq) . (n + 1)) + ((X,seq,Cseq) . ((n + 1) + 1))) is Element of the U1 of X
(Partial_Sums seq) . (n + 1) is Element of the U1 of X
Cseq . (n + 1) is V11() Element of COMPLEX
(Cseq . (n + 1)) * ((Partial_Sums seq) . (n + 1)) is Element of the U1 of X
((Cseq . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + ((X,seq,Cseq) . ((n + 1) + 1)) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n) + (((Cseq . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + ((X,seq,Cseq) . ((n + 1) + 1))) is Element of the U1 of X
Cseq . ((n + 1) + 1) is V11() Element of COMPLEX
(Cseq . (n + 1)) - (Cseq . ((n + 1) + 1)) is V11() Element of COMPLEX
((Cseq . (n + 1)) - (Cseq . ((n + 1) + 1))) + (Cseq . ((n + 1) + 1)) is V11() Element of COMPLEX
(((Cseq . (n + 1)) - (Cseq . ((n + 1) + 1))) + (Cseq . ((n + 1) + 1))) * ((Partial_Sums seq) . (n + 1)) is Element of the U1 of X
seq . ((n + 1) + 1) is Element of the U1 of X
(Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)) is Element of the U1 of X
((((Cseq . (n + 1)) - (Cseq . ((n + 1) + 1))) + (Cseq . ((n + 1) + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n) + (((((Cseq . (n + 1)) - (Cseq . ((n + 1) + 1))) + (Cseq . ((n + 1) + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the U1 of X
((Cseq . (n + 1)) - (Cseq . ((n + 1) + 1))) * ((Partial_Sums seq) . (n + 1)) is Element of the U1 of X
(Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)) is Element of the U1 of X
(((Cseq . (n + 1)) - (Cseq . ((n + 1) + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) is Element of the U1 of X
((((Cseq . (n + 1)) - (Cseq . ((n + 1) + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n) + (((((Cseq . (n + 1)) - (Cseq . ((n + 1) + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the U1 of X
(Cseq ^\ 1) . (n + 1) is V11() Element of COMPLEX
(Cseq . (n + 1)) - ((Cseq ^\ 1) . (n + 1)) is V11() Element of COMPLEX
((Cseq . (n + 1)) - ((Cseq ^\ 1) . (n + 1))) * ((Partial_Sums seq) . (n + 1)) is Element of the U1 of X
(((Cseq . (n + 1)) - ((Cseq ^\ 1) . (n + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) is Element of the U1 of X
((((Cseq . (n + 1)) - ((Cseq ^\ 1) . (n + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n) + (((((Cseq . (n + 1)) - ((Cseq ^\ 1) . (n + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the U1 of X
- ((Cseq ^\ 1) . (n + 1)) is V11() Element of COMPLEX
(Cseq . (n + 1)) + (- ((Cseq ^\ 1) . (n + 1))) is V11() Element of COMPLEX
((Cseq . (n + 1)) + (- ((Cseq ^\ 1) . (n + 1)))) * ((Partial_Sums seq) . (n + 1)) is Element of the U1 of X
(((Cseq . (n + 1)) + (- ((Cseq ^\ 1) . (n + 1)))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) is Element of the U1 of X
((((Cseq . (n + 1)) + (- ((Cseq ^\ 1) . (n + 1)))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n) + (((((Cseq . (n + 1)) + (- ((Cseq ^\ 1) . (n + 1)))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the U1 of X
(- (Cseq ^\ 1)) . (n + 1) is V11() Element of COMPLEX
(Cseq . (n + 1)) + ((- (Cseq ^\ 1)) . (n + 1)) is V11() Element of COMPLEX
((Cseq . (n + 1)) + ((- (Cseq ^\ 1)) . (n + 1))) * ((Partial_Sums seq) . (n + 1)) is Element of the U1 of X
(((Cseq . (n + 1)) + ((- (Cseq ^\ 1)) . (n + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) is Element of the U1 of X
((((Cseq . (n + 1)) + ((- (Cseq ^\ 1)) . (n + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n) + (((((Cseq . (n + 1)) + ((- (Cseq ^\ 1)) . (n + 1))) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the U1 of X
(Cseq - (Cseq ^\ 1)) . (n + 1) is V11() Element of COMPLEX
((Cseq - (Cseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1)) is Element of the U1 of X
(((Cseq - (Cseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) is Element of the U1 of X
((((Cseq - (Cseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n) + (((((Cseq - (Cseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1)))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the U1 of X
((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))) is Element of the U1 of X
(((Cseq - (Cseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + (((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n) + ((((Cseq - (Cseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1))) + (((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1))))) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n) + (((Cseq - (Cseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1))) is Element of the U1 of X
(((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n) + (((Cseq - (Cseq ^\ 1)) . (n + 1)) * ((Partial_Sums seq) . (n + 1)))) + (((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the U1 of X
(X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1))) . (n + 1) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n) + ((X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1))) . (n + 1)) is Element of the U1 of X
(((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n) + ((X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1))) . (n + 1))) + (((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the U1 of X
(Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . (n + 1) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . (n + 1)) + (((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . (n + 1))) + ((Cseq . ((n + 1) + 1)) * (seq . ((n + 1) + 1)))) is Element of the U1 of X
((Partial_Sums seq) . (n + 1)) + (seq . ((n + 1) + 1)) is Element of the U1 of X
(Cseq . ((n + 1) + 1)) * (((Partial_Sums seq) . (n + 1)) + (seq . ((n + 1) + 1))) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . (n + 1)) + ((Cseq . ((n + 1) + 1)) * (((Partial_Sums seq) . (n + 1)) + (seq . ((n + 1) + 1)))) is Element of the U1 of X
(Partial_Sums seq) . ((n + 1) + 1) is Element of the U1 of X
(Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . ((n + 1) + 1)) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . (n + 1)) + ((Cseq . ((n + 1) + 1)) * ((Partial_Sums seq) . ((n + 1) + 1))) is Element of the U1 of X
(X,(Partial_Sums seq),Cseq) . ((n + 1) + 1) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . (n + 1)) + ((X,(Partial_Sums seq),Cseq) . ((n + 1) + 1)) is Element of the U1 of X
((Partial_Sums (X,seq,Cseq)) . ((n + 1) + 1)) - ((X,(Partial_Sums seq),Cseq) . ((n + 1) + 1)) is Element of the U1 of X
- ((X,(Partial_Sums seq),Cseq) . ((n + 1) + 1)) is Element of the U1 of X
K298(X,((Partial_Sums (X,seq,Cseq)) . ((n + 1) + 1)),(- ((X,(Partial_Sums seq),Cseq) . ((n + 1) + 1)))) is Element of the U1 of X
((X,(Partial_Sums seq),Cseq) . ((n + 1) + 1)) - ((X,(Partial_Sums seq),Cseq) . ((n + 1) + 1)) is Element of the U1 of X
K298(X,((X,(Partial_Sums seq),Cseq) . ((n + 1) + 1)),(- ((X,(Partial_Sums seq),Cseq) . ((n + 1) + 1)))) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . (n + 1)) + (((X,(Partial_Sums seq),Cseq) . ((n + 1) + 1)) - ((X,(Partial_Sums seq),Cseq) . ((n + 1) + 1))) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . (n + 1)) + H₁(X) is Element of the U1 of X
(Partial_Sums (X,seq,Cseq)) . (0 + 1) is Element of the U1 of X
(Partial_Sums (X,seq,Cseq)) . 0 is Element of the U1 of X
(X,seq,Cseq) . (0 + 1) is Element of the U1 of X
((Partial_Sums (X,seq,Cseq)) . 0) + ((X,seq,Cseq) . (0 + 1)) is Element of the U1 of X
(X,seq,Cseq) . 0 is Element of the U1 of X
(X,seq,Cseq) . 1 is Element of the U1 of X
((X,seq,Cseq) . 0) + ((X,seq,Cseq) . 1) is Element of the U1 of X
((Cseq . 0) * (seq . 0)) + ((X,seq,Cseq) . 1) is Element of the U1 of X
((Cseq . 0) * (seq . 0)) + ((Cseq . 1) * (seq . 1)) is Element of the U1 of X
((Cseq . 0) * (seq . 0)) + H₁(X) is Element of the U1 of X
(((Cseq . 0) * (seq . 0)) + H₁(X)) + ((Cseq . 1) * (seq . 1)) is Element of the U1 of X
((Cseq . 1) * (seq . 0)) - ((Cseq . 1) * (seq . 0)) is Element of the U1 of X
K298(X,((Cseq . 1) * (seq . 0)),(- ((Cseq . 1) * (seq . 0)))) is Element of the U1 of X
((Cseq . 0) * (seq . 0)) + (((Cseq . 1) * (seq . 0)) - ((Cseq . 1) * (seq . 0))) is Element of the U1 of X
(((Cseq . 0) * (seq . 0)) + (((Cseq . 1) * (seq . 0)) - ((Cseq . 1) * (seq . 0)))) + ((Cseq . 1) * (seq . 1)) is Element of the U1 of X
((Cseq . 0) * (seq . 0)) + (- ((Cseq . 1) * (seq . 0))) is Element of the U1 of X
(((Cseq . 0) * (seq . 0)) + (- ((Cseq . 1) * (seq . 0)))) + ((Cseq . 1) * (seq . 0)) is Element of the U1 of X
((((Cseq . 0) * (seq . 0)) + (- ((Cseq . 1) * (seq . 0)))) + ((Cseq . 1) * (seq . 0))) + ((Cseq . 1) * (seq . 1)) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . 0) + ((X,(Partial_Sums seq),Cseq) . (0 + 1)) is Element of the U1 of X
((Partial_Sums (X,seq,Cseq)) . (0 + 1)) - ((X,(Partial_Sums seq),Cseq) . (0 + 1)) is Element of the U1 of X
- ((X,(Partial_Sums seq),Cseq) . (0 + 1)) is Element of the U1 of X
K298(X,((Partial_Sums (X,seq,Cseq)) . (0 + 1)),(- ((X,(Partial_Sums seq),Cseq) . (0 + 1)))) is Element of the U1 of X
((X,(Partial_Sums seq),Cseq) . (0 + 1)) - ((X,(Partial_Sums seq),Cseq) . (0 + 1)) is Element of the U1 of X
K298(X,((X,(Partial_Sums seq),Cseq) . (0 + 1)),(- ((X,(Partial_Sums seq),Cseq) . (0 + 1)))) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . 0) + (((X,(Partial_Sums seq),Cseq) . (0 + 1)) - ((X,(Partial_Sums seq),Cseq) . (0 + 1))) is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . 0) + 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))
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( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
(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 (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,(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))
Cseq ^\ 1 is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued subsequence of Cseq
(Cseq ^\ 1) - Cseq is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
- Cseq is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
- 1 is V1() V11() V12() ext-real non positive negative integer set
(- 1) (#) Cseq is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
(Cseq ^\ 1) + (- Cseq) is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
(X,(Partial_Sums seq),((Cseq ^\ 1) - 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 (X,(Partial_Sums seq),((Cseq ^\ 1) - 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 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 (X,seq,Cseq)) . (n + 1) is Element of the U1 of X
(X,(Partial_Sums seq),Cseq) . (n + 1) is Element of the U1 of X
(Partial_Sums (X,(Partial_Sums seq),((Cseq ^\ 1) - Cseq))) . n is Element of the U1 of X
((X,(Partial_Sums seq),Cseq) . (n + 1)) - ((Partial_Sums (X,(Partial_Sums seq),((Cseq ^\ 1) - Cseq))) . n) is Element of the U1 of X
- ((Partial_Sums (X,(Partial_Sums seq),((Cseq ^\ 1) - Cseq))) . n) is Element of the U1 of X
K298(X,((X,(Partial_Sums seq),Cseq) . (n + 1)),(- ((Partial_Sums (X,(Partial_Sums seq),((Cseq ^\ 1) - Cseq))) . n))) is Element of the U1 of X
Cseq - (Cseq ^\ 1) is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
- (Cseq ^\ 1) is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
(- 1) (#) (Cseq ^\ 1) is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
Cseq + (- (Cseq ^\ 1)) is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
(X,(Partial_Sums seq),(Cseq - (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 (X,(Partial_Sums seq),(Cseq - (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 (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n is Element of the U1 of X
((Partial_Sums (X,(Partial_Sums seq),(Cseq - (Cseq ^\ 1)))) . n) + ((X,(Partial_Sums seq),Cseq) . (n + 1)) is Element of the U1 of X
((Partial_Sums (X,seq,Cseq)) . (n + 1)) - ((X,(Partial_Sums seq),Cseq) . (n + 1)) is Element of the U1 of X
- ((X,(Partial_Sums seq),Cseq) . (n + 1)) is Element of the U1 of X
K298(X,((Partial_Sums (X,seq,Cseq)) . (n + 1)),(- ((X,(Partial_Sums seq),Cseq) . (n + 1)))) is Element of the U1 of X
(((Partial_Sums (X,seq,Cseq)) . (n + 1)) - ((X,(Partial_Sums seq),Cseq) . (n + 1))) + ((X,(Partial_Sums seq),Cseq) . (n + 1)) is Element of the U1 of X
((X,(Partial_Sums seq),Cseq) . (n + 1)) - ((X,(Partial_Sums seq),Cseq) . (n + 1)) is Element of the U1 of X
K298(X,((X,(Partial_Sums seq),Cseq) . (n + 1)),(- ((X,(Partial_Sums seq),Cseq) . (n + 1)))) is Element of the U1 of X
((Partial_Sums (X,seq,Cseq)) . (n + 1)) - (((X,(Partial_Sums seq),Cseq) . (n + 1)) - ((X,(Partial_Sums seq),Cseq) . (n + 1))) is Element of the U1 of X
- (((X,(Partial_Sums seq),Cseq) . (n + 1)) - ((X,(Partial_Sums seq),Cseq) . (n + 1))) is Element of the U1 of X
K298(X,((Partial_Sums (X,seq,Cseq)) . (n + 1)),(- (((X,(Partial_Sums seq),Cseq) . (n + 1)) - ((X,(Partial_Sums seq),Cseq) . (n + 1))))) is Element of the U1 of X
0. X is V82(X) Element of the U1 of X
((Partial_Sums (X,seq,Cseq)) . (n + 1)) - H₁(X) is Element of the U1 of X
- (0. X) is Element of the U1 of X
K298(X,((Partial_Sums (X,seq,Cseq)) . (n + 1)),(- (0. X))) is Element of the U1 of X
- (Cseq ^\ 1) is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
Cseq + (- (Cseq ^\ 1)) is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
(X,(Partial_Sums seq),(Cseq + (- (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 (X,(Partial_Sums seq),(Cseq + (- (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 (X,(Partial_Sums seq),(Cseq + (- (Cseq ^\ 1))))) . n is Element of the U1 of X
((X,(Partial_Sums seq),Cseq) . (n + 1)) + ((Partial_Sums (X,(Partial_Sums seq),(Cseq + (- (Cseq ^\ 1))))) . n) is Element of the U1 of X
(- 1r) (#) (Cseq ^\ 1) is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
- Cseq is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
((- 1r) (#) (Cseq ^\ 1)) - (- Cseq) is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
- (- Cseq) is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
(- 1) (#) (- Cseq) is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
((- 1r) (#) (Cseq ^\ 1)) + (- (- Cseq)) is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
(X,(Partial_Sums seq),(((- 1r) (#) (Cseq ^\ 1)) - (- 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 (X,(Partial_Sums seq),(((- 1r) (#) (Cseq ^\ 1)) - (- 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 (X,(Partial_Sums seq),(((- 1r) (#) (Cseq ^\ 1)) - (- Cseq)))) . n is Element of the U1 of X
((X,(Partial_Sums seq),Cseq) . (n + 1)) + ((Partial_Sums (X,(Partial_Sums seq),(((- 1r) (#) (Cseq ^\ 1)) - (- Cseq)))) . n) is Element of the U1 of X
(- 1r) (#) Cseq is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
((- 1r) (#) (Cseq ^\ 1)) - ((- 1r) (#) Cseq) is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
- ((- 1r) (#) Cseq) is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
(- 1) (#) ((- 1r) (#) Cseq) is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
((- 1r) (#) (Cseq ^\ 1)) + (- ((- 1r) (#) Cseq)) is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
(X,(Partial_Sums seq),(((- 1r) (#) (Cseq ^\ 1)) - ((- 1r) (#) 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 (X,(Partial_Sums seq),(((- 1r) (#) (Cseq ^\ 1)) - ((- 1r) (#) 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 (X,(Partial_Sums seq),(((- 1r) (#) (Cseq ^\ 1)) - ((- 1r) (#) Cseq)))) . n is Element of the U1 of X
((X,(Partial_Sums seq),Cseq) . (n + 1)) + ((Partial_Sums (X,(Partial_Sums seq),(((- 1r) (#) (Cseq ^\ 1)) - ((- 1r) (#) Cseq)))) . n) is Element of the U1 of X
(- 1r) (#) ((Cseq ^\ 1) - Cseq) is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
(X,(Partial_Sums seq),((- 1r) (#) ((Cseq ^\ 1) - 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 (X,(Partial_Sums seq),((- 1r) (#) ((Cseq ^\ 1) - 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 (X,(Partial_Sums seq),((- 1r) (#) ((Cseq ^\ 1) - Cseq)))) . n is Element of the U1 of X
((X,(Partial_Sums seq),Cseq) . (n + 1)) + ((Partial_Sums (X,(Partial_Sums seq),((- 1r) (#) ((Cseq ^\ 1) - Cseq)))) . n) is Element of the U1 of X
(- 1r) * (X,(Partial_Sums seq),((Cseq ^\ 1) - 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 ((- 1r) * (X,(Partial_Sums seq),((Cseq ^\ 1) - 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 ((- 1r) * (X,(Partial_Sums seq),((Cseq ^\ 1) - Cseq)))) . n is Element of the U1 of X
((X,(Partial_Sums seq),Cseq) . (n + 1)) + ((Partial_Sums ((- 1r) * (X,(Partial_Sums seq),((Cseq ^\ 1) - Cseq)))) . n) is Element of the U1 of X
(- 1r) * (Partial_Sums (X,(Partial_Sums seq),((Cseq ^\ 1) - 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))
((- 1r) * (Partial_Sums (X,(Partial_Sums seq),((Cseq ^\ 1) - Cseq)))) . n is Element of the U1 of X
((X,(Partial_Sums seq),Cseq) . (n + 1)) + (((- 1r) * (Partial_Sums (X,(Partial_Sums seq),((Cseq ^\ 1) - Cseq)))) . n) is Element of the U1 of X
(- 1r) * ((Partial_Sums (X,(Partial_Sums seq),((Cseq ^\ 1) - Cseq))) . n) is Element of the U1 of X
((X,(Partial_Sums seq),Cseq) . (n + 1)) + ((- 1r) * ((Partial_Sums (X,(Partial_Sums seq),((Cseq ^\ 1) - Cseq))) . 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))
Cseq is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
(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))
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
(X,(X,seq,Cseq),(n + 1)) is Element of the U1 of X
Partial_Sums (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 (X,seq,Cseq)) . (n + 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))
(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))
(X,(Partial_Sums seq),Cseq) . (n + 1) is Element of the U1 of X
Cseq ^\ 1 is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued subsequence of Cseq
(Cseq ^\ 1) - Cseq is V1() V13() V16( NAT ) V17( COMPLEX ) V18() V23( NAT ) V27( NAT , COMPLEX ) complex-valued Element of K6(K7(NAT,COMPLEX))
- Cseq is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
- 1 is V1() V11() V12() ext-real non positive negative integer set
(- 1) (#) Cseq is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
(Cseq ^\ 1) + (- Cseq) is V13() V16( NAT ) V18() V23( NAT ) complex-valued set
(X,(Partial_Sums seq),((Cseq ^\ 1) - 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,(X,(Partial_Sums seq),((Cseq ^\ 1) - Cseq)),n) is Element of the U1 of X
Partial_Sums (X,(Partial_Sums seq),((Cseq ^\ 1) - 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 (X,(Partial_Sums seq),((Cseq ^\ 1) - Cseq))) . n is Element of the U1 of X
((X,(Partial_Sums seq),Cseq) . (n + 1)) - (X,(X,(Partial_Sums seq),((Cseq ^\ 1) - Cseq)),n) is Element of the U1 of X
- (X,(X,(Partial_Sums seq),((Cseq ^\ 1) - Cseq)),n) is Element of the U1 of X
K298(X,((X,(Partial_Sums seq),Cseq) . (n + 1)),(- (X,(X,(Partial_Sums seq),((Cseq ^\ 1) - Cseq)),n))) is Element of the U1 of X