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₁[ 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₁[i,y]

proof

let i be Nat; :: thesis: ( i in Seg n implies ex y being Element of REAL st S₁[i,y] )
assume A3: i in Seg n ; :: thesis: ex y being Element of REAL st S₁[i,y]
deffunc H₁( Nat) -> set = (xvseq . $1) . i;
consider rseqi being Real_Sequence such that
A4: for l being Nat holds rseqi . l = H₁(l) from SEQ_1:sch 1();
reconsider lr = lim rseqi as Element of REAL by XREAL_0:def 1;
take lr ; :: thesis: S₁[i,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 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;

end;

then rseqi is convergent by SEQ_4:41;
hence S₁[i,lr] by A4; :: thesis: verum

end;

consider f being FinSequence of REAL such that
A9: ( dom f = Seg n & ( for k being Nat st k in Seg n holds
S₁[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₁[k,f . k] by A9;
hence vseq is convergent by A10, Th11; :: thesis: verum