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

let vseq be sequence of (); :: 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 S1[ 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 S1[i,y]
proof
let i be Nat; :: thesis: ( i in Seg n implies ex y being Element of REAL st S1[i,y] )
assume A3: i in Seg n ; :: thesis: ex y being Element of REAL st S1[i,y]
deffunc H1( Nat) -> set = (xvseq . \$1) . i;
consider rseqi being Real_Sequence such that
A4: for l being Nat holds rseqi . l = H1(l) from SEQ_1:sch 1();
reconsider lr = lim rseqi as Element of REAL by XREAL_0:def 1;
take lr ; :: thesis: S1[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 ;
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 ;
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 ; :: thesis: verum
end;
end;
then rseqi is convergent by SEQ_4:41;
hence S1[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
S1[k,f . k] ) ) from reconsider tseq = f as Element of REAL n by ;
reconsider xseq = tseq as Point of () by Def4;
A10: xseq = tseq ;
for k being Nat st k in Seg n holds
S1[k,f . k] by A9;
hence vseq is convergent by ; :: thesis: verum