let vseq be sequence of l2_Space ; :: thesis: ( vseq is Cauchy implies vseq is convergent )
assume A1: vseq is Cauchy ; :: thesis: vseq is convergent
defpred S₁[ set , set ] means ex i being Element of NAT st
( $1 = i & ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & $2 = lim rseqi ) );
A2: for x being set st x in NAT holds
ex y being set st
( y in REAL & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in REAL & S₁[x,y] ) )
assume A3: x in NAT ; :: thesis: ex y being set st
( y in REAL & S₁[x,y] )
reconsider i = x as Element of NAT by A3;
deffunc H₁( set ) -> Element of REAL = (seq_id (vseq . $1)) . i;
consider rseqi being Real_Sequence such that
A4: for n being Element of NAT holds rseqi . n = H₁(n) from SEQ_1:sch 1();
A5: rseqi is convergent

proof

now

let e be real number ; :: thesis: ( e > 0 implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e )
assume A6: e > 0 ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e
thus ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e :: thesis: verum

proof

e is Real by XREAL_0:def 1;
then consider k being Element of NAT such that
A7: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A6, BHSP_3:2;

now

let m be Element of NAT ; :: thesis: ( k <= m implies abs ((rseqi . m) - (rseqi . k)) < e )
assume A8: k <= m ; :: thesis: abs ((rseqi . m) - (rseqi . k)) < e
||.((vseq . m) - (vseq . k)).|| < e by A7, A8;
then A9: sqrt (((vseq . m) - (vseq . k)) .|. ((vseq . m) - (vseq . k))) < e by BHSP_1:def 4;
reconsider e1 = e as Real by XREAL_0:def 1;
A10: (seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k))) is summable by RSSPACE:def 11, RSSPACE:def 13;
A11: for i being Element of NAT holds 0 <= ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) . i

proof

let i be Element of NAT ; :: thesis: 0 <= ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) . i
((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) . i = ((seq_id ((vseq . m) - (vseq . k))) . i) * ((seq_id ((vseq . m) - (vseq . k))) . i) by SEQ_1:12;
hence 0 <= ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) . i by XREAL_1:65; :: thesis: verum

end;

then A12: 0 <= Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) by A10, SERIES_1:21;
then A13: 0 <= sqrt (Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k))))) by SQUARE_1:def 4;
sqrt (Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k))))) < e by A9, Th1;
then (sqrt (Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))))) ^2 < e1 ^2 by A13, SQUARE_1:78;
then A14: Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) < e * e by A12, SQUARE_1:def 4;
A15: (abs ((rseqi . m) - (rseqi . k))) * (abs ((rseqi . m) - (rseqi . k))) = ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) . i

proof

seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th1
.= (seq_id (vseq . m)) - (seq_id (vseq . k)) by RSSPACE:3
.= (seq_id (vseq . m)) + (- (seq_id (vseq . k))) by SEQ_1:15 ;
then (seq_id ((vseq . m) - (vseq . k))) . i = ((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i) by SEQ_1:11
.= ((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i)) by SEQ_1:14
.= ((seq_id (vseq . m)) . i) - ((seq_id (vseq . k)) . i)
.= (rseqi . m) - ((seq_id (vseq . k)) . i) by A4
.= (rseqi . m) - (rseqi . k) by A4 ;
then ((seq_id ((vseq . m) - (vseq . k))) . i) * ((seq_id ((vseq . m) - (vseq . k))) . i) = ((rseqi . m) - (rseqi . k)) ^2
.= (abs ((rseqi . m) - (rseqi . k))) ^2 by COMPLEX1:161
.= (abs ((rseqi . m) - (rseqi . k))) * (abs ((rseqi . m) - (rseqi . k))) ;
hence (abs ((rseqi . m) - (rseqi . k))) * (abs ((rseqi . m) - (rseqi . k))) = ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) . i by SEQ_1:12; :: thesis: verum

end;

A16: ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) . i <= Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) by A10, A11, Lm1;
0 <= abs ((rseqi . m) - (rseqi . k)) by COMPLEX1:132;
then A17: 0 <= (abs ((rseqi . m) - (rseqi . k))) * (abs ((rseqi . m) - (rseqi . k))) ;
A18: (abs ((rseqi . m) - (rseqi . k))) * (abs ((rseqi . m) - (rseqi . k))) < e * e by A14, A15, A16, XXREAL_0:2;
A19: sqrt ((abs ((rseqi . m) - (rseqi . k))) * (abs ((rseqi . m) - (rseqi . k)))) = sqrt ((abs ((rseqi . m) - (rseqi . k))) ^2 )
.= abs ((rseqi . m) - (rseqi . k)) by COMPLEX1:132, SQUARE_1:89 ;
sqrt (e * e) = sqrt (e1 ^2 )
.= e by A6, SQUARE_1:89 ;
hence abs ((rseqi . m) - (rseqi . k)) < e by A17, A18, A19, SQUARE_1:95; :: thesis: verum

end;

hence ex k being Element of NAT st
for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e ; :: thesis: verum

end;

end;

hence rseqi is convergent by SEQ_4:58; :: thesis: verum

end;

take lim rseqi ; :: thesis: ( lim rseqi in REAL & S₁[x, lim rseqi] )
thus ( lim rseqi in REAL & S₁[x, lim rseqi] ) by A4, A5; :: thesis: verum

end;

consider f being Function of NAT ,REAL such that
A20: for x being set st x in NAT holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);
reconsider tseq = f as Real_Sequence ;

A21: now

let i be Element of NAT ; :: thesis: ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi )
reconsider x = i as set ;
ex i0 being Element of NAT st
( x = i0 & ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i0 ) & rseqi is convergent & f . x = lim rseqi ) ) by A20;
hence ex rseqi being Real_Sequence st
( ( for n being Element of NAT holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi ) ; :: thesis: verum

end;

A22: for e being Real st e > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( ((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) < e * e )

proof

let e1 be Real; :: thesis: ( e1 > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( ((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) < e1 * e1 ) )
assume A23: e1 > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( ((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) < e1 * e1 )
set e = e1 / 2;
A24: e1 / 2 > 0 by A23, XREAL_1:217;
e1 / 2 < e1 by A23, XREAL_1:218;
then A25: (e1 / 2) * (e1 / 2) < e1 * e1 by A24, XREAL_1:99;
consider k being Element of NAT such that
A26: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e1 / 2 by A1, A24, BHSP_3:2;
A27: for m, n being Element of NAT st n >= k & m >= k holds
( (seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m))) is summable & Sum ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) < (e1 / 2) * (e1 / 2) & ( for i being Element of NAT holds 0 <= ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) . i ) )

proof

let m, n be Element of NAT ; :: thesis: ( n >= k & m >= k implies ( (seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m))) is summable & Sum ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) < (e1 / 2) * (e1 / 2) & ( for i being Element of NAT holds 0 <= ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) . i ) ) )
assume A28: ( n >= k & m >= k ) ; :: thesis: ( (seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m))) is summable & Sum ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) < (e1 / 2) * (e1 / 2) & ( for i being Element of NAT holds 0 <= ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) . i ) )
||.((vseq . n) - (vseq . m)).|| < e1 / 2 by A26, A28;
then A29: sqrt (((vseq . n) - (vseq . m)) .|. ((vseq . n) - (vseq . m))) < e1 / 2 by BHSP_1:def 4;
A30: (seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m))) is summable by RSSPACE:def 11, RSSPACE:def 13;
A31: for i being Element of NAT holds 0 <= ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) . i

proof

let i be Element of NAT ; :: thesis: 0 <= ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) . i
((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) . i = ((seq_id ((vseq . n) - (vseq . m))) . i) * ((seq_id ((vseq . n) - (vseq . m))) . i) by SEQ_1:12;
hence 0 <= ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) . i by XREAL_1:65; :: thesis: verum

end;

then A32: 0 <= Sum ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) by A30, SERIES_1:21;
then A33: 0 <= sqrt (Sum ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m))))) by SQUARE_1:def 4;
sqrt (Sum ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m))))) < e1 / 2 by A29, Th1;
then (sqrt (Sum ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))))) ^2 < (e1 / 2) ^2 by A33, SQUARE_1:78;
hence ( (seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m))) is summable & Sum ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) < (e1 / 2) * (e1 / 2) & ( for i being Element of NAT holds 0 <= ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) . i ) ) by A31, A32, RSSPACE:def 11, RSSPACE:def 13, SQUARE_1:def 4; :: thesis: verum

end;

A34: for n, i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i )

proof

let n be Element of NAT ; :: thesis: for i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i )
A35: for m, k being Element of NAT holds seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))

proof

let m, k be Element of NAT ; :: thesis: seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k))
thus seq_id ((vseq . m) - (vseq . k)) = seq_id ((seq_id (vseq . m)) - (seq_id (vseq . k))) by Th1
.= (seq_id (vseq . m)) - (seq_id (vseq . k)) by RSSPACE:3 ; :: thesis: verum

end;

defpred S₂[ Nat] means for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . $1 ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . $1 );
A36: S₂[ 0 ]

proof

now

let rseq be Real_Sequence; :: thesis: ( ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . 0 ) implies ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . 0 ) )
assume A37: for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . 0 ; :: thesis: ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . 0 )
thus ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . 0 ) :: thesis: verum

proof

consider rseq0 being Real_Sequence such that
A38: ( ( for m being Element of NAT holds rseq0 . m = (seq_id (vseq . m)) . 0 ) & rseq0 is convergent & tseq . 0 = lim rseq0 ) by A21;

A39: now

let m be Element of NAT ; :: thesis: rseq . m = ((rseq0 . m) - ((seq_id (vseq . n)) . 0 )) * ((rseq0 . m) - ((seq_id (vseq . n)) . 0 ))
thus rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . 0 by A37
.= ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n)))) . 0 by SERIES_1:def 1
.= (((seq_id (vseq . m)) - (seq_id (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n)))) . 0 by A35
.= (((seq_id (vseq . m)) - (seq_id (vseq . n))) (#) ((seq_id (vseq . m)) - (seq_id (vseq . n)))) . 0 by A35
.= (((seq_id (vseq . m)) - (seq_id (vseq . n))) . 0 ) * (((seq_id (vseq . m)) - (seq_id (vseq . n))) . 0 ) by SEQ_1:12
.= (((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0 ) * (((seq_id (vseq . m)) - (seq_id (vseq . n))) . 0 ) by SEQ_1:15
.= (((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0 ) * (((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0 ) by SEQ_1:15
.= (((seq_id (vseq . m)) . 0 ) + ((- (seq_id (vseq . n))) . 0 )) * (((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . 0 ) by SEQ_1:11
.= (((seq_id (vseq . m)) . 0 ) + ((- (seq_id (vseq . n))) . 0 )) * (((seq_id (vseq . m)) . 0 ) + ((- (seq_id (vseq . n))) . 0 )) by SEQ_1:11
.= (((seq_id (vseq . m)) . 0 ) + (- ((seq_id (vseq . n)) . 0 ))) * (((seq_id (vseq . m)) . 0 ) + ((- (seq_id (vseq . n))) . 0 )) by SEQ_1:14
.= (((seq_id (vseq . m)) . 0 ) - ((seq_id (vseq . n)) . 0 )) * (((seq_id (vseq . m)) . 0 ) + (- ((seq_id (vseq . n)) . 0 ))) by SEQ_1:14
.= ((rseq0 . m) - ((seq_id (vseq . n)) . 0 )) * (((seq_id (vseq . m)) . 0 ) - ((seq_id (vseq . n)) . 0 )) by A38
.= ((rseq0 . m) - ((seq_id (vseq . n)) . 0 )) * ((rseq0 . m) - ((seq_id (vseq . n)) . 0 )) by A38 ; :: thesis: verum

end;

then lim rseq = ((tseq . 0 ) + (- ((seq_id (vseq . n)) . 0 ))) * ((tseq . 0 ) - ((seq_id (vseq . n)) . 0 )) by A38, Lm4
.= ((tseq . 0 ) + ((- (seq_id (vseq . n))) . 0 )) * ((tseq . 0 ) + (- ((seq_id (vseq . n)) . 0 ))) by SEQ_1:14
.= ((tseq . 0 ) + ((- (seq_id (vseq . n))) . 0 )) * ((tseq . 0 ) + ((- (seq_id (vseq . n))) . 0 )) by SEQ_1:14
.= ((tseq + (- (seq_id (vseq . n)))) . 0 ) * ((tseq . 0 ) + ((- (seq_id (vseq . n))) . 0 )) by SEQ_1:11
.= ((tseq + (- (seq_id (vseq . n)))) . 0 ) * ((tseq + (- (seq_id (vseq . n)))) . 0 ) by SEQ_1:11
.= ((tseq - (seq_id (vseq . n))) . 0 ) * ((tseq + (- (seq_id (vseq . n)))) . 0 ) by SEQ_1:15
.= ((tseq - (seq_id (vseq . n))) . 0 ) * ((tseq - (seq_id (vseq . n))) . 0 ) by SEQ_1:15
.= ((tseq - (seq_id (vseq . n))) (#) (tseq - (seq_id (vseq . n)))) . 0 by SEQ_1:12
.= (Partial_Sums ((tseq - (seq_id (vseq . n))) (#) (tseq - (seq_id (vseq . n))))) . 0 by SERIES_1:def 1
.= (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) (tseq - (seq_id (vseq . n))))) . 0 by RSSPACE:3
.= (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . 0 by RSSPACE:3 ;
hence ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . 0 ) by A38, A39, Lm4; :: thesis: verum

end;

end;

hence S₂[ 0 ] ; :: thesis: verum

end;

A40: for i being Element of NAT st S₂[i] holds
S₂[i + 1]

proof

now

let i be Element of NAT ; :: thesis: ( ( for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i ) ) implies for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . (i + 1) ) )
assume A41: for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i ) ; :: thesis: for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . (i + 1) )
thus for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . (i + 1) ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . (i + 1) ) :: thesis: verum

proof

let rseq be Real_Sequence; :: thesis: ( ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . (i + 1) ) implies ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . (i + 1) ) )
assume A42: for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . (i + 1) ; :: thesis: ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . (i + 1) )
deffunc H₁( Element of NAT ) -> Element of REAL = (Partial_Sums ((seq_id ((vseq . $1) - (vseq . n))) (#) (seq_id ((vseq . $1) - (vseq . n))))) . i;
consider rseqb being Real_Sequence such that
A43: for m being Element of NAT holds rseqb . m = H₁(m) from SEQ_1:sch 1();
A44: ( rseqb is convergent & lim rseqb = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i ) by A41, A43;
consider rseq0 being Real_Sequence such that
A45: ( ( for m being Element of NAT holds rseq0 . m = (seq_id (vseq . m)) . (i + 1) ) & rseq0 is convergent & tseq . (i + 1) = lim rseq0 ) by A21;

A46: now

let m be Element of NAT ; :: thesis: rseq . m = (((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1))) * ((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1)))) + (rseqb . m)
thus rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . (i + 1) by A42
.= (((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n)))) . (i + 1)) + ((Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . i) by SERIES_1:def 1
.= ((((seq_id (vseq . m)) - (seq_id (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n)))) . (i + 1)) + ((Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . i) by A35
.= ((((seq_id (vseq . m)) - (seq_id (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n)))) . (i + 1)) + (rseqb . m) by A43
.= ((((seq_id (vseq . m)) - (seq_id (vseq . n))) (#) ((seq_id (vseq . m)) - (seq_id (vseq . n)))) . (i + 1)) + (rseqb . m) by A35
.= ((((seq_id (vseq . m)) - (seq_id (vseq . n))) . (i + 1)) * (((seq_id (vseq . m)) - (seq_id (vseq . n))) . (i + 1))) + (rseqb . m) by SEQ_1:12
.= ((((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . (i + 1)) * (((seq_id (vseq . m)) - (seq_id (vseq . n))) . (i + 1))) + (rseqb . m) by SEQ_1:15
.= ((((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . (i + 1)) * (((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . (i + 1))) + (rseqb . m) by SEQ_1:15
.= ((((seq_id (vseq . m)) . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))) * (((seq_id (vseq . m)) + (- (seq_id (vseq . n)))) . (i + 1))) + (rseqb . m) by SEQ_1:11
.= ((((seq_id (vseq . m)) . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))) * (((seq_id (vseq . m)) . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1)))) + (rseqb . m) by SEQ_1:11
.= ((((seq_id (vseq . m)) . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1)))) * (((seq_id (vseq . m)) . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1)))) + (rseqb . m) by SEQ_1:14
.= ((((seq_id (vseq . m)) . (i + 1)) - ((seq_id (vseq . n)) . (i + 1))) * (((seq_id (vseq . m)) . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1))))) + (rseqb . m) by SEQ_1:14
.= (((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1))) * (((seq_id (vseq . m)) . (i + 1)) - ((seq_id (vseq . n)) . (i + 1)))) + (rseqb . m) by A45
.= (((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1))) * ((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1)))) + (rseqb . m) by A45 ; :: thesis: verum

end;

then lim rseq = (((tseq . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1)))) * ((tseq . (i + 1)) - ((seq_id (vseq . n)) . (i + 1)))) + (lim rseqb) by A44, A45, Lm5
.= (((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))) * ((tseq . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1))))) + (lim rseqb) by SEQ_1:14
.= (((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))) * ((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1)))) + (lim rseqb) by SEQ_1:14
.= (((tseq + (- (seq_id (vseq . n)))) . (i + 1)) * ((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1)))) + (lim rseqb) by SEQ_1:11
.= (((tseq + (- (seq_id (vseq . n)))) . (i + 1)) * ((tseq + (- (seq_id (vseq . n)))) . (i + 1))) + (lim rseqb) by SEQ_1:11
.= (((tseq - (seq_id (vseq . n))) . (i + 1)) * ((tseq + (- (seq_id (vseq . n)))) . (i + 1))) + (lim rseqb) by SEQ_1:15
.= (((tseq - (seq_id (vseq . n))) . (i + 1)) * ((tseq - (seq_id (vseq . n))) . (i + 1))) + (lim rseqb) by SEQ_1:15
.= (((tseq - (seq_id (vseq . n))) (#) (tseq - (seq_id (vseq . n)))) . (i + 1)) + (lim rseqb) by SEQ_1:12
.= (((tseq - (seq_id (vseq . n))) (#) (tseq - (seq_id (vseq . n)))) . (i + 1)) + ((Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i) by A41, A43
.= (((tseq - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) . (i + 1)) + ((Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i) by RSSPACE:3
.= ((((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) . (i + 1)) + ((Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i) by RSSPACE:3
.= (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . (i + 1) by SERIES_1:def 1 ;
hence ( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . (i + 1) ) by A44, A45, A46, Lm5; :: thesis: verum

end;

end;

hence for i being Element of NAT st S₂[i] holds
S₂[i + 1] ; :: thesis: verum

end;

for i being Element of NAT holds S₂[i] from NAT_1:sch 1(A36, A40);
hence for i being Element of NAT
for rseq being Real_Sequence st ( for m being Element of NAT holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . i ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i ) ; :: thesis: verum

end;

for n being Element of NAT st n >= k holds
( ((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) < e1 * e1 )

proof

let n be Element of NAT ; :: thesis: ( n >= k implies ( ((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) < e1 * e1 ) )
assume A47: n >= k ; :: thesis: ( ((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) < e1 * e1 )
A48: for i being Element of NAT st 0 <= i holds
(Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i <= (e1 / 2) * (e1 / 2)

proof

let i be Element of NAT ; :: thesis: ( 0 <= i implies (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i <= (e1 / 2) * (e1 / 2) )
assume 0 <= i ; :: thesis: (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i <= (e1 / 2) * (e1 / 2)
deffunc H₁( Element of NAT ) -> Element of REAL = (Partial_Sums ((seq_id ((vseq . $1) - (vseq . n))) (#) (seq_id ((vseq . $1) - (vseq . n))))) . i;
consider rseq being Real_Sequence such that
A49: for m being Element of NAT holds rseq . m = H₁(m) from SEQ_1:sch 1();
A50: rseq is convergent by A34, A49;
A51: lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i by A34, A49;
for m being Element of NAT st m >= k holds
rseq . m <= (e1 / 2) * (e1 / 2)

proof

let m be Element of NAT ; :: thesis: ( m >= k implies rseq . m <= (e1 / 2) * (e1 / 2) )
assume A52: m >= k ; :: thesis: rseq . m <= (e1 / 2) * (e1 / 2)
A53: rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . i by A49;
A54: ( (seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))) is summable & Sum ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n)))) < (e1 / 2) * (e1 / 2) & ( for i being Element of NAT holds 0 <= ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n)))) . i ) ) by A27, A47, A52;
then (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . i <= Sum ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n)))) by Lm1;
hence rseq . m <= (e1 / 2) * (e1 / 2) by A53, A54, XXREAL_0:2; :: thesis: verum

end;

hence (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i <= (e1 / 2) * (e1 / 2) by A50, A51, Lm3; :: thesis: verum

end;

A55: for i being Element of NAT holds 0 <= (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) . i

proof

let i be Element of NAT ; :: thesis: 0 <= (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) . i
(((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) . i = (((seq_id tseq) - (seq_id (vseq . n))) . i) * (((seq_id tseq) - (seq_id (vseq . n))) . i) by SEQ_1:12;
hence 0 <= (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) . i by XREAL_1:65; :: thesis: verum

end;

A56: Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) is bounded_above

proof

now

let i be Element of NAT ; :: thesis: (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i < e1 * e1
(Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i <= (e1 / 2) * (e1 / 2) by A48;
hence (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i < e1 * e1 by A25, XXREAL_0:2; :: thesis: verum

end;

hence Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) is bounded_above by SEQ_2:def 3; :: thesis: verum

end;

then ((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))) is summable by A55, SERIES_1:20;
then A57: Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) is convergent by SERIES_1:def 2;
A58: Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) = lim (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) by SERIES_1:def 3;
lim (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) <= (e1 / 2) * (e1 / 2) by A48, A57, Lm3;
hence ( ((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) < e1 * e1 ) by A25, A55, A56, A58, SERIES_1:20, XXREAL_0:2; :: thesis: verum

end;

hence ex k being Element of NAT st
for n being Element of NAT st n >= k holds
( ((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) < e1 * e1 ) ; :: thesis: verum

end;

A59: (seq_id tseq) (#) (seq_id tseq) is summable

proof

A60: for i being Element of NAT holds 0 <= ((seq_id tseq) (#) (seq_id tseq)) . i

proof

let i be Element of NAT ; :: thesis: 0 <= ((seq_id tseq) (#) (seq_id tseq)) . i
((seq_id tseq) (#) (seq_id tseq)) . i = ((seq_id tseq) . i) * ((seq_id tseq) . i) by SEQ_1:12;
hence 0 <= ((seq_id tseq) (#) (seq_id tseq)) . i by XREAL_1:65; :: thesis: verum

end;

consider m being Element of NAT such that
A61: for n being Element of NAT st n >= m holds
( ((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) < 1 * 1 ) by A22;
A62: ((seq_id tseq) - (seq_id (vseq . m))) (#) ((seq_id tseq) - (seq_id (vseq . m))) is summable by A61;
A63: (seq_id (vseq . m)) (#) (seq_id (vseq . m)) is summable by RSSPACE:def 11, RSSPACE:def 13;
set a = ((seq_id tseq) - (seq_id (vseq . m))) (#) ((seq_id tseq) - (seq_id (vseq . m)));
set b = (seq_id (vseq . m)) (#) (seq_id (vseq . m));
set d = (seq_id tseq) (#) (seq_id tseq);
A64: 2 (#) (((seq_id tseq) - (seq_id (vseq . m))) (#) ((seq_id tseq) - (seq_id (vseq . m)))) is summable by A62, SERIES_1:13;
2 (#) ((seq_id (vseq . m)) (#) (seq_id (vseq . m))) is summable by A63, SERIES_1:13;
then A65: (2 (#) (((seq_id tseq) - (seq_id (vseq . m))) (#) ((seq_id tseq) - (seq_id (vseq . m))))) + (2 (#) ((seq_id (vseq . m)) (#) (seq_id (vseq . m)))) is summable by A64, SERIES_1:10;
for i being Element of NAT holds ((seq_id tseq) (#) (seq_id tseq)) . i <= ((2 (#) (((seq_id tseq) - (seq_id (vseq . m))) (#) ((seq_id tseq) - (seq_id (vseq . m))))) + (2 (#) ((seq_id (vseq . m)) (#) (seq_id (vseq . m))))) . i

proof

let i be Element of NAT ; :: thesis: ((seq_id tseq) (#) (seq_id tseq)) . i <= ((2 (#) (((seq_id tseq) - (seq_id (vseq . m))) (#) ((seq_id tseq) - (seq_id (vseq . m))))) + (2 (#) ((seq_id (vseq . m)) (#) (seq_id (vseq . m))))) . i
A66: ((seq_id tseq) (#) (seq_id tseq)) . i = ((seq_id tseq) . i) * ((seq_id tseq) . i) by SEQ_1:12;
A67: ((2 (#) (((seq_id tseq) - (seq_id (vseq . m))) (#) ((seq_id tseq) - (seq_id (vseq . m))))) + (2 (#) ((seq_id (vseq . m)) (#) (seq_id (vseq . m))))) . i = ((2 (#) (((seq_id tseq) - (seq_id (vseq . m))) (#) ((seq_id tseq) - (seq_id (vseq . m))))) . i) + ((2 (#) ((seq_id (vseq . m)) (#) (seq_id (vseq . m)))) . i) by SEQ_1:11
.= (2 * ((((seq_id tseq) - (seq_id (vseq . m))) (#) ((seq_id tseq) - (seq_id (vseq . m)))) . i)) + ((2 (#) ((seq_id (vseq . m)) (#) (seq_id (vseq . m)))) . i) by SEQ_1:13
.= (2 * ((((seq_id tseq) - (seq_id (vseq . m))) (#) ((seq_id tseq) - (seq_id (vseq . m)))) . i)) + (2 * (((seq_id (vseq . m)) (#) (seq_id (vseq . m))) . i)) by SEQ_1:13 ;
((seq_id tseq) - (seq_id (vseq . m))) . i = ((seq_id tseq) + (- (seq_id (vseq . m)))) . i by SEQ_1:15
.= ((seq_id tseq) . i) + ((- (seq_id (vseq . m))) . i) by SEQ_1:11
.= ((seq_id tseq) . i) + (- ((seq_id (vseq . m)) . i)) by SEQ_1:14
.= ((seq_id tseq) . i) - ((seq_id (vseq . m)) . i) ;
then A68: (((seq_id tseq) - (seq_id (vseq . m))) (#) ((seq_id tseq) - (seq_id (vseq . m)))) . i = (((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)) * (((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)) by SEQ_1:12;
set x = (seq_id tseq) . i;
set y = (seq_id (vseq . m)) . i;
A69: 2 * ((((seq_id tseq) - (seq_id (vseq . m))) (#) ((seq_id tseq) - (seq_id (vseq . m)))) . i) = (2 * (((seq_id tseq) . i) - ((seq_id (vseq . m)) . i))) * (((seq_id tseq) . i) - ((seq_id (vseq . m)) . i)) by A68;
2 * (((seq_id (vseq . m)) (#) (seq_id (vseq . m))) . i) = 2 * (((seq_id (vseq . m)) . i) * ((seq_id (vseq . m)) . i)) by SEQ_1:12
.= (2 * ((seq_id (vseq . m)) . i)) * ((seq_id (vseq . m)) . i) ;
hence ((seq_id tseq) (#) (seq_id tseq)) . i <= ((2 (#) (((seq_id tseq) - (seq_id (vseq . m))) (#) ((seq_id tseq) - (seq_id (vseq . m))))) + (2 (#) ((seq_id (vseq . m)) (#) (seq_id (vseq . m))))) . i by A66, A67, A69, Lm2; :: thesis: verum

end;

hence (seq_id tseq) (#) (seq_id tseq) is summable by A60, A65, SERIES_1:24; :: thesis: verum

end;

tseq in the_set_of_RealSequences by RSSPACE:def 1;
then reconsider tv = tseq as Point of l2_Space by A59, RSSPACE:def 11, RSSPACE:def 13;
for e being Real st e > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e

proof

let e be Real; :: thesis: ( e > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e )
assume A70: e > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e
consider m being Element of NAT such that
A71: for n being Element of NAT st n >= m holds
( ((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))) is summable & Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) < e * e ) by A22, A70;

now

let n be Element of NAT ; :: thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume A72: n >= m ; :: thesis: ||.((vseq . n) - tv).|| < e
A73: Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) < e * e by A71, A72;
tseq in the_set_of_RealSequences by RSSPACE:def 1;
then reconsider u = tseq as VECTOR of l2_Space by A59, RSSPACE:def 11, RSSPACE:def 13;
reconsider v = vseq . n as VECTOR of l2_Space ;
seq_id (u - v) = u - v by Th1;
then seq_id (u - v) = (seq_id tseq) - (seq_id (vseq . n)) by Th1;
then A74: (u - v) .|. (u - v) < e * e by A73, Th1;
0 <= (u - v) .|. (u - v) by BHSP_1:def 2;
then A75: sqrt ((u - v) .|. (u - v)) < sqrt (e ^2 ) by A74, SQUARE_1:95;
||.((vseq . n) - tv).|| = ||.(- (tv - (vseq . n))).|| by RLVECT_1:47
.= ||.(tv - (vseq . n)).|| by BHSP_1:37
.= sqrt ((u - v) .|. (u - v)) by BHSP_1:def 4 ;
hence ||.((vseq . n) - tv).|| < e by A70, A75, SQUARE_1:89; :: thesis: verum

end;

hence ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((vseq . n) - tv).|| < e ; :: thesis: verum

end;

hence vseq is convergent by BHSP_2:9; :: thesis: verum