let vseq be sequence of l2_Space; :: according to BHSP_3:def 4 :: thesis: ( not vseq is Cauchy or vseq is convergent )
assume A1: vseq is Cauchy ; :: thesis: vseq is convergent
defpred S₁[ object , object ] means ex i being Nat st
( c₁ = i & ex rseqi being Real_Sequence st
( ( for n being Nat holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & c₂ = lim rseqi ) );
A2: for x being object st x in NAT holds
ex y being object st
( y in REAL & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in NAT implies ex y being object st
( y in REAL & S₁[x,y] ) )
assume x in NAT ; :: thesis: ex y being object st
( y in REAL & S₁[x,y] )
then reconsider i = x as Element of NAT ;
deffunc H₁( set ) -> Element of REAL = (seq_id (vseq . c₁)) . i;
consider rseqi being Real_Sequence such that
A3: for n being Nat holds rseqi . n = H₁(n) from SEQ_1:sch 1();
reconsider lr = lim rseqi as Element of REAL by XREAL_0:def 1;
take lr ; :: thesis: ( lr in REAL & S₁[x,lr] )

now :: thesis: for e being Real st e > 0 holds
ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e

let e be Real; :: thesis: ( e > 0 implies ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e )
assume A4: e > 0 ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e
thus ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e :: thesis: verum

proof

consider k being Nat such that
A5: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A4, BHSP_3:2;

now :: thesis: for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e

let m be Nat; :: thesis: ( k <= m implies |.((rseqi . m) - (rseqi . k)).| < e )
assume k <= m ; :: thesis: |.((rseqi . m) - (rseqi . k)).| < e
then ||.((vseq . m) - (vseq . k)).|| < e by A5;
then sqrt (((vseq . m) - (vseq . k)) .|. ((vseq . m) - (vseq . k))) < e by BHSP_1:def 4;
then A6: sqrt (Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k))))) < e by Th1;
reconsider e1 = e as Real ;
A7: sqrt (|.((rseqi . m) - (rseqi . k)).| * |.((rseqi . m) - (rseqi . k)).|) = sqrt (|.((rseqi . m) - (rseqi . k)).| ^2)
.= |.((rseqi . m) - (rseqi . k)).| by COMPLEX1:46, SQUARE_1:22 ;
seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k)) by Th1
.= (seq_id (vseq . m)) + (- (seq_id (vseq . k))) by SEQ_1:11 ;
then (seq_id ((vseq . m) - (vseq . k))) . i = ((seq_id (vseq . m)) . i) + ((- (seq_id (vseq . k))) . i) by SEQ_1:7
.= ((seq_id (vseq . m)) . i) + (- ((seq_id (vseq . k)) . i)) by SEQ_1:10
.= ((seq_id (vseq . m)) . i) - ((seq_id (vseq . k)) . i)
.= (rseqi . m) - ((seq_id (vseq . k)) . i) by A3
.= (rseqi . m) - (rseqi . k) by A3 ;
then ((seq_id ((vseq . m) - (vseq . k))) . i) * ((seq_id ((vseq . m) - (vseq . k))) . i) = ((rseqi . m) - (rseqi . k)) ^2
.= |.((rseqi . m) - (rseqi . k)).| ^2 by COMPLEX1:75
.= |.((rseqi . m) - (rseqi . k)).| * |.((rseqi . m) - (rseqi . k)).| ;
then A8: |.((rseqi . m) - (rseqi . k)).| * |.((rseqi . m) - (rseqi . k)).| = ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) . i by SEQ_1:8;
A9: for i being Nat holds 0 <= ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) . i

proof

let i be 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:8;
hence 0 <= ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) . i by XREAL_1:63; :: thesis: verum

end;

A10: (seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k))) is summable by RSSPACE:def 11;
then A11: 0 <= Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) by A9, SERIES_1:18;
then 0 <= sqrt (Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k))))) by SQUARE_1:def 2;
then (sqrt (Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))))) ^2 < e1 ^2 by A6, SQUARE_1:16;
then A12: Sum ((seq_id ((vseq . m) - (vseq . k))) (#) (seq_id ((vseq . m) - (vseq . k)))) < e * e by A11, SQUARE_1:def 2;
((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, A9, Lm1;
then A13: ( 0 <= |.((rseqi . m) - (rseqi . k)).| & |.((rseqi . m) - (rseqi . k)).| * |.((rseqi . m) - (rseqi . k)).| < e * e ) by A12, A8, COMPLEX1:46, XXREAL_0:2;
sqrt (e * e) = sqrt (e1 ^2)
.= e by A4, SQUARE_1:22 ;
hence |.((rseqi . m) - (rseqi . k)).| < e by A13, A7, SQUARE_1:27; :: thesis: verum

end;

hence ex k being Nat st
for m being Nat st k <= m holds
|.((rseqi . m) - (rseqi . k)).| < e ; :: thesis: verum

end;

end;

then rseqi is convergent by SEQ_4:41;
hence ( lr in REAL & S₁[x,lr] ) by A3; :: thesis: verum

end;

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

A15: now :: thesis: for i being Nat ex rseqi being Real_Sequence st
( ( for n being Nat holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi )

let i be Nat; :: thesis: ex rseqi being Real_Sequence st
( ( for n being Nat holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi )
i in NAT by ORDINAL1:def 12;
then ex i0 being Nat st
( i = i0 & ex rseqi being Real_Sequence st
( ( for n being Nat holds rseqi . n = (seq_id (vseq . n)) . i0 ) & rseqi is convergent & f . i = lim rseqi ) ) by A14;
hence ex rseqi being Real_Sequence st
( ( for n being Nat holds rseqi . n = (seq_id (vseq . n)) . i ) & rseqi is convergent & tseq . i = lim rseqi ) ; :: thesis: verum

end;

A16: for e being Real st e > 0 holds
ex k being Nat st
for n being 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 Nat st
for n being 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 A17: e1 > 0 ; :: thesis: ex k being Nat st
for n being 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;
A18: e1 / 2 > 0 by A17, XREAL_1:215;
then consider k being Nat such that
A19: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e1 / 2 by A1, BHSP_3:2;
e1 / 2 < e1 by A17, XREAL_1:216;
then A20: (e1 / 2) * (e1 / 2) < e1 * e1 by A18, XREAL_1:97;
A21: for m, n being 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 Nat holds 0 <= ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) . i ) )

proof

let m, n be 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 Nat holds 0 <= ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) . i ) ) )
assume ( 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 Nat holds 0 <= ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) . i ) )
then ||.((vseq . n) - (vseq . m)).|| < e1 / 2 by A19;
then sqrt (((vseq . n) - (vseq . m)) .|. ((vseq . n) - (vseq . m))) < e1 / 2 by BHSP_1:def 4;
then A22: sqrt (Sum ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m))))) < e1 / 2 by Th1;
A23: for i being Nat holds 0 <= ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) . i

proof

let i be 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:8;
hence 0 <= ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) . i by XREAL_1:63; :: thesis: verum

end;

(seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m))) is summable by RSSPACE:def 11;
then A24: 0 <= Sum ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) by A23, SERIES_1:18;
then 0 <= sqrt (Sum ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m))))) by SQUARE_1:def 2;
then (sqrt (Sum ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))))) ^2 < (e1 / 2) ^2 by A22, SQUARE_1:16;
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 Nat holds 0 <= ((seq_id ((vseq . n) - (vseq . m))) (#) (seq_id ((vseq . n) - (vseq . m)))) . i ) ) by A23, A24, RSSPACE:def 11, SQUARE_1:def 2; :: thesis: verum

end;

A25: for n, i being Nat
for rseq being Real_Sequence st ( for m being 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 Nat; :: thesis: for i being Nat
for rseq being Real_Sequence st ( for m being 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 )
defpred S₂[ Nat] means for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . c₁ ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . c₁ );
A26: for m, k being Nat holds seq_id ((vseq . m) - (vseq . k)) = (seq_id (vseq . m)) - (seq_id (vseq . k)) by Th1;
for i being Nat st S₂[i] holds
S₂[i + 1]

proof

let i be Nat; :: thesis: ( S₂[i] implies S₂[i + 1] )
assume A27: for rseq being Real_Sequence st ( for m being 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: S₂[i + 1]
thus for rseq being Real_Sequence st ( for m being 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

deffunc H₁( Nat) -> Element of REAL = (Partial_Sums ((seq_id ((vseq . c₁) - (vseq . n))) (#) (seq_id ((vseq . c₁) - (vseq . n))))) . i;
consider rseqb being Real_Sequence such that
A28: for m being Nat holds rseqb . m = H₁(m) from SEQ_1:sch 1();
consider rseq0 being Real_Sequence such that
A29: for m being Nat holds rseq0 . m = (seq_id (vseq . m)) . (i + 1) and
A30: rseq0 is convergent and
A31: tseq . (i + 1) = lim rseq0 by A15;
let rseq be Real_Sequence; :: thesis: ( ( for m being 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 A32: for m being 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) )

A33: now :: thesis: for m being Nat holds rseq . m = (((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1))) * ((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1)))) + (rseqb . m)

let m be 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 A32
.= (((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 A26
.= ((((seq_id (vseq . m)) - (seq_id (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n)))) . (i + 1)) + (rseqb . m) by A28
.= ((((seq_id (vseq . m)) - (seq_id (vseq . n))) (#) ((seq_id (vseq . m)) - (seq_id (vseq . n)))) . (i + 1)) + (rseqb . m) by A26
.= ((((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:8
.= ((((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:11
.= ((((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:7, 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:7
.= ((((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:10
.= ((((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:10
.= (((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1))) * (((seq_id (vseq . m)) . (i + 1)) - ((seq_id (vseq . n)) . (i + 1)))) + (rseqb . m) by A29
.= (((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1))) * ((rseq0 . m) - ((seq_id (vseq . n)) . (i + 1)))) + (rseqb . m) by A29 ; :: thesis: verum

end;

A34: rseqb is convergent by A27, A28;
then lim rseq = (((tseq . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1)))) * ((tseq . (i + 1)) - ((seq_id (vseq . n)) . (i + 1)))) + (lim rseqb) by A30, A31, A33, Lm5
.= (((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))) * ((tseq . (i + 1)) + (- ((seq_id (vseq . n)) . (i + 1))))) + (lim rseqb) by SEQ_1:10
.= (((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1))) * ((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1)))) + (lim rseqb) by SEQ_1:10
.= (((tseq + (- (seq_id (vseq . n)))) . (i + 1)) * ((tseq . (i + 1)) + ((- (seq_id (vseq . n))) . (i + 1)))) + (lim rseqb) by SEQ_1:7
.= (((tseq - (seq_id (vseq . n))) . (i + 1)) * ((tseq + (- (seq_id (vseq . n)))) . (i + 1))) + (lim rseqb) by SEQ_1:7, 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))) (#) (tseq - (seq_id (vseq . n)))) . (i + 1)) + (lim rseqb) by SEQ_1:8
.= (((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 A27, A28
.= (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 A34, A30, A33, Lm5; :: thesis: verum

end;

end;

then A35: for i being Nat st S₂[i] holds
S₂[i + 1] ;

now :: thesis: for rseq being Real_Sequence st ( for m being Nat holds rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . 0 ) holds
( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . 0 )

let rseq be Real_Sequence; :: thesis: ( ( for m being 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 A36: for m being 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
A37: for m being Nat holds rseq0 . m = (seq_id (vseq . m)) . 0 and
A38: rseq0 is convergent and
A39: tseq . 0 = lim rseq0 by A15;

A40: now :: thesis: for m being Nat holds rseq . m = ((rseq0 . m) - ((seq_id (vseq . n)) . 0)) * ((rseq0 . m) - ((seq_id (vseq . n)) . 0))

let m be 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 A36
.= ((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 A26
.= (((seq_id (vseq . m)) - (seq_id (vseq . n))) (#) ((seq_id (vseq . m)) - (seq_id (vseq . n)))) . 0 by A26
.= (((seq_id (vseq . m)) - (seq_id (vseq . n))) . 0) * (((seq_id (vseq . m)) - (seq_id (vseq . n))) . 0) by SEQ_1:8
.= (((seq_id (vseq . m)) + (- (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)) + (- (seq_id (vseq . n)))) . 0) by SEQ_1:7, 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:7
.= (((seq_id (vseq . m)) . 0) + (- ((seq_id (vseq . n)) . 0))) * (((seq_id (vseq . m)) . 0) + ((- (seq_id (vseq . n))) . 0)) by SEQ_1:10
.= (((seq_id (vseq . m)) . 0) - ((seq_id (vseq . n)) . 0)) * (((seq_id (vseq . m)) . 0) + (- ((seq_id (vseq . n)) . 0))) by SEQ_1:10
.= ((rseq0 . m) - ((seq_id (vseq . n)) . 0)) * (((seq_id (vseq . m)) . 0) - ((seq_id (vseq . n)) . 0)) by A37
.= ((rseq0 . m) - ((seq_id (vseq . n)) . 0)) * ((rseq0 . m) - ((seq_id (vseq . n)) . 0)) by A37 ; :: thesis: verum

end;

then lim rseq = ((tseq . 0) + (- ((seq_id (vseq . n)) . 0))) * ((tseq . 0) - ((seq_id (vseq . n)) . 0)) by A38, A39, Lm4
.= ((tseq . 0) + ((- (seq_id (vseq . n))) . 0)) * ((tseq . 0) + (- ((seq_id (vseq . n)) . 0))) by SEQ_1:10
.= ((tseq . 0) + ((- (seq_id (vseq . n))) . 0)) * ((tseq . 0) + ((- (seq_id (vseq . n))) . 0)) by SEQ_1:10
.= ((tseq + (- (seq_id (vseq . n)))) . 0) * ((tseq . 0) + ((- (seq_id (vseq . n))) . 0)) by SEQ_1:7
.= ((tseq - (seq_id (vseq . n))) . 0) * ((tseq + (- (seq_id (vseq . n)))) . 0) by SEQ_1:7, SEQ_1:11
.= ((tseq - (seq_id (vseq . n))) . 0) * ((tseq - (seq_id (vseq . n))) . 0) by SEQ_1:11
.= ((tseq - (seq_id (vseq . n))) (#) (tseq - (seq_id (vseq . n)))) . 0 by SEQ_1:8
.= (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . 0 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))))) . 0 ) by A38, A40, Lm4; :: thesis: verum

end;

end;

then A41: S₂[ 0 ] ;
for i being Nat holds S₂[i] from NAT_1:sch 2(A41, A35);
hence for i being Nat
for rseq being Real_Sequence st ( for m being 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 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 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 A42: 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 )
A43: for i being 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 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₁( Nat) -> Element of REAL = (Partial_Sums ((seq_id ((vseq . c₁) - (vseq . n))) (#) (seq_id ((vseq . c₁) - (vseq . n))))) . i;
consider rseq being Real_Sequence such that
A44: for m being Nat holds rseq . m = H₁(m) from SEQ_1:sch 1();
A45: for m being Nat st m >= k holds
rseq . m <= (e1 / 2) * (e1 / 2)

proof

let m be Nat; :: thesis: ( m >= k implies rseq . m <= (e1 / 2) * (e1 / 2) )
assume A46: m >= k ; :: thesis: rseq . m <= (e1 / 2) * (e1 / 2)
( (seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))) is summable & ( for i being Nat holds 0 <= ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n)))) . i ) ) by A21, A42, A46;
then A47: (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;
A48: rseq . m = (Partial_Sums ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n))))) . i by A44;
Sum ((seq_id ((vseq . m) - (vseq . n))) (#) (seq_id ((vseq . m) - (vseq . n)))) < (e1 / 2) * (e1 / 2) by A21, A42, A46;
hence rseq . m <= (e1 / 2) * (e1 / 2) by A48, A47, XXREAL_0:2; :: thesis: verum

end;

( rseq is convergent & lim rseq = (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i ) by A25, A44;
hence (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i <= (e1 / 2) * (e1 / 2) by A45, Lm3; :: thesis: verum

end;

now :: thesis: for i being Nat holds (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i < e1 * e1

let i be 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 A43;
hence (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) . i < e1 * e1 by A20, XXREAL_0:2; :: thesis: verum

end;

then A49: Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) is bounded_above by SEQ_2:def 3;
A50: for i being Nat holds 0 <= (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) . i

proof

let i be 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:8;
hence 0 <= (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) . i by XREAL_1:63; :: thesis: verum

end;

then ((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))) is summable by A49, SERIES_1:17;
then Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) is convergent by SERIES_1:def 2;
then ( 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))))) & lim (Partial_Sums (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n))))) <= (e1 / 2) * (e1 / 2) ) by A43, Lm3, SERIES_1:def 3;
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 A20, A50, A49, SERIES_1:17, XXREAL_0:2; :: thesis: verum

end;

hence ex k being Nat st
for n being 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;

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

proof

set d = (seq_id tseq) (#) (seq_id tseq);
A52: for i being Nat holds 0 <= ((seq_id tseq) (#) (seq_id tseq)) . i

proof

let i be 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:8;
hence 0 <= ((seq_id tseq) (#) (seq_id tseq)) . i by XREAL_1:63; :: thesis: verum

end;

consider m being Nat such that
A53: for n being 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 A16;
set b = (seq_id (vseq . m)) (#) (seq_id (vseq . m));
set a = ((seq_id tseq) - (seq_id (vseq . m))) (#) ((seq_id tseq) - (seq_id (vseq . m)));
(seq_id (vseq . m)) (#) (seq_id (vseq . m)) is summable by RSSPACE:def 11;
then A54: 2 (#) ((seq_id (vseq . m)) (#) (seq_id (vseq . m))) is summable by SERIES_1:10;
A55: for i being 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 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
set x = (seq_id tseq) . i;
set y = (seq_id (vseq . m)) . i;
A56: 2 * (((seq_id (vseq . m)) (#) (seq_id (vseq . m))) . i) = 2 * (((seq_id (vseq . m)) . i) * ((seq_id (vseq . m)) . i)) by SEQ_1:8
.= (2 * ((seq_id (vseq . m)) . i)) * ((seq_id (vseq . m)) . i) ;
((seq_id tseq) - (seq_id (vseq . m))) . i = ((seq_id tseq) + (- (seq_id (vseq . m)))) . i by SEQ_1:11
.= ((seq_id tseq) . i) + ((- (seq_id (vseq . m))) . i) by SEQ_1:7
.= ((seq_id tseq) . i) + (- ((seq_id (vseq . m)) . i)) by SEQ_1:10
.= ((seq_id tseq) . i) - ((seq_id (vseq . m)) . i) ;
then (((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:8;
then A57: ( ((seq_id tseq) (#) (seq_id tseq)) . i = ((seq_id tseq) . i) * ((seq_id tseq) . i) & 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 SEQ_1:8;
((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:7
.= (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:9
.= (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:9 ;
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 A57, A56, Lm2; :: thesis: verum

end;

((seq_id tseq) - (seq_id (vseq . m))) (#) ((seq_id tseq) - (seq_id (vseq . m))) is summable by A53;
then 2 (#) (((seq_id tseq) - (seq_id (vseq . m))) (#) ((seq_id tseq) - (seq_id (vseq . m)))) is summable by SERIES_1:10;
then (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 A54, SERIES_1:7;
hence (seq_id tseq) (#) (seq_id tseq) is summable by A52, A55, SERIES_1:20; :: thesis: verum

end;

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

proof

let e be Real; :: thesis: ( e > 0 implies ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e )
assume A58: e > 0 ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e
consider m being Nat such that
A59: for n being 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 A16, A58;

now :: thesis: for n being Nat st n >= m holds
||.((vseq . n) - tv).|| < e

tseq in the_set_of_RealSequences by FUNCT_2:8;
then reconsider u = tseq as VECTOR of l2_Space by A51, RSSPACE:def 11;
let n be Nat; :: thesis: ( n >= m implies ||.((vseq . n) - tv).|| < e )
assume n >= m ; :: thesis: ||.((vseq . n) - tv).|| < e
then A60: Sum (((seq_id tseq) - (seq_id (vseq . n))) (#) ((seq_id tseq) - (seq_id (vseq . n)))) < e * e by A59;
reconsider v = vseq . n as VECTOR of l2_Space ;
seq_id (u - v) = (seq_id tseq) - (seq_id (vseq . n)) by Th1;
then A61: (u - v) .|. (u - v) < e * e by A60, Th1;
A62: ||.((vseq . n) - tv).|| = ||.(- (tv - (vseq . n))).|| by RLVECT_1:33
.= ||.(tv - (vseq . n)).|| by BHSP_1:31
.= sqrt ((u - v) .|. (u - v)) by BHSP_1:def 4 ;
0 <= (u - v) .|. (u - v) by BHSP_1:def 2;
then sqrt ((u - v) .|. (u - v)) < sqrt (e ^2) by A61, SQUARE_1:27;
hence ||.((vseq . n) - tv).|| < e by A58, A62, SQUARE_1:22; :: thesis: verum

end;

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

end;

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