let n be Nat; :: thesis: for f being sequence of (REAL-NS n) st f is Cauchy_sequence_by_Norm holds

f is convergent

let vseq be sequence of (REAL-NS n); :: thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )

assume A1: vseq is Cauchy_sequence_by_Norm ; :: thesis: vseq is convergent

reconsider xvseq = vseq as sequence of (REAL n) by Def4;

defpred S_{1}[ set , set ] means ex rseqi being Real_Sequence st

for l being Nat holds

( rseqi . l = (xvseq . l) . $1 & rseqi is convergent & $2 = lim rseqi );

A2: for i being Nat st i in Seg n holds

ex y being Element of REAL st S_{1}[i,y]

A9: ( dom f = Seg n & ( for k being Nat st k in Seg n holds

S_{1}[k,f . k] ) )
from FINSEQ_1:sch 5(A2);

reconsider tseq = f as Element of REAL n by A9, Th6;

reconsider xseq = tseq as Point of (REAL-NS n) by Def4;

A10: xseq = tseq ;

for k being Nat st k in Seg n holds

S_{1}[k,f . k]
by A9;

hence vseq is convergent by A10, Th11; :: thesis: verum

f is convergent

let vseq be sequence of (REAL-NS n); :: thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )

assume A1: vseq is Cauchy_sequence_by_Norm ; :: thesis: vseq is convergent

reconsider xvseq = vseq as sequence of (REAL n) by Def4;

defpred S

for l being Nat holds

( rseqi . l = (xvseq . l) . $1 & rseqi is convergent & $2 = lim rseqi );

A2: for i being Nat st i in Seg n holds

ex y being Element of REAL st S

proof

consider f being FinSequence of REAL such that
let i be Nat; :: thesis: ( i in Seg n implies ex y being Element of REAL st S_{1}[i,y] )

assume A3: i in Seg n ; :: thesis: ex y being Element of REAL st S_{1}[i,y]

deffunc H_{1}( Nat) -> set = (xvseq . $1) . i;

consider rseqi being Real_Sequence such that

A4: for l being Nat holds rseqi . l = H_{1}(l)
from SEQ_1:sch 1();

reconsider lr = lim rseqi as Element of REAL by XREAL_0:def 1;

take lr ; :: thesis: S_{1}[i,lr]

hence S_{1}[i,lr]
by A4; :: thesis: verum

end;assume A3: i in Seg n ; :: thesis: ex y being Element of REAL st S

deffunc H

consider rseqi being Real_Sequence such that

A4: for l being Nat holds rseqi . l = H

reconsider lr = lim rseqi as Element of REAL by XREAL_0:def 1;

take lr ; :: thesis: S

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

then
rseqi is convergent
by SEQ_4:41;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 A5: 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

end;for m being Nat st k <= m holds

|.((rseqi . m) - (rseqi . k)).| < e )

assume A5: 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

A6: for n, m being Nat st n >= k & m >= k holds

||.((vseq . n) - (vseq . m)).|| < e by A1, A5, RSSPACE3:8;

take k ; :: 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 A7: ||.((vseq . m) - (vseq . k)).|| < e by A6;

len ((xvseq . m) - (xvseq . k)) = n by CARD_1:def 7;

then i in dom ((xvseq . m) - (xvseq . k)) by A3, FINSEQ_1:def 3;

then ((xvseq . m) . i) - ((xvseq . k) . i) = ((xvseq . m) - (xvseq . k)) . i by VALUED_1:13;

then A8: |.(((xvseq . m) . i) - ((xvseq . k) . i)).| <= ||.((vseq . m) - (vseq . k)).|| by A3, Th5, Th9;

( rseqi . m = (xvseq . m) . i & rseqi . k = (xvseq . k) . i ) by A4;

hence |.((rseqi . m) - (rseqi . k)).| < e by A7, A8, XXREAL_0:2; :: thesis: verum

end;A6: for n, m being Nat st n >= k & m >= k holds

||.((vseq . n) - (vseq . m)).|| < e by A1, A5, RSSPACE3:8;

take k ; :: 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 A7: ||.((vseq . m) - (vseq . k)).|| < e by A6;

len ((xvseq . m) - (xvseq . k)) = n by CARD_1:def 7;

then i in dom ((xvseq . m) - (xvseq . k)) by A3, FINSEQ_1:def 3;

then ((xvseq . m) . i) - ((xvseq . k) . i) = ((xvseq . m) - (xvseq . k)) . i by VALUED_1:13;

then A8: |.(((xvseq . m) . i) - ((xvseq . k) . i)).| <= ||.((vseq . m) - (vseq . k)).|| by A3, Th5, Th9;

( rseqi . m = (xvseq . m) . i & rseqi . k = (xvseq . k) . i ) by A4;

hence |.((rseqi . m) - (rseqi . k)).| < e by A7, A8, XXREAL_0:2; :: thesis: verum

hence S

A9: ( dom f = Seg n & ( for k being Nat st k in Seg n holds

S

reconsider tseq = f as Element of REAL n by A9, Th6;

reconsider xseq = tseq as Point of (REAL-NS n) by Def4;

A10: xseq = tseq ;

for k being Nat st k in Seg n holds

S

hence vseq is convergent by A10, Th11; :: thesis: verum