let n be Nat; :: thesis: for f being sequence of (REAL-NS n) st f is CCauchy holds
f is convergent
let vseq be sequence of (REAL-NS n); :: thesis: ( vseq is CCauchy implies vseq is convergent )
assume A1: vseq is CCauchy ; :: thesis: vseq is convergent
reconsider xvseq = vseq as Function of NAT,(REAL n) by Def4;
defpred S₁[ set , set ] means ex rseqi being Real_Sequence st
for l being Element of 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₁( Element of NAT ) -> Element of REAL = (xvseq . $1) . i;
consider rseqi being Real_Sequence such that
A4: for l being Element of NAT holds rseqi . l = H₁(l) from SEQ_1:sch 1();
take lim rseqi ; :: thesis: S₁[i, lim rseqi]

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 A5: 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
A6: for n, m being Element of NAT st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A5, RSSPACE3:10;
take k ; :: thesis: for m being Element of NAT st k <= m holds
abs ((rseqi . m) - (rseqi . k)) < e
let m be Element of NAT ; :: thesis: ( k <= m implies abs ((rseqi . m) - (rseqi . k)) < e )
assume k <= m ; :: thesis: abs ((rseqi . m) - (rseqi . k)) < e
then A7: ||.((vseq . m) - (vseq . k)).|| < e by A6;
len ((xvseq . m) - (xvseq . k)) = n by FINSEQ_1:def 18;
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: abs (((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 abs ((rseqi . m) - (rseqi . k)) < e by A7, A8, XXREAL_0:2; :: thesis: verum

end;

end;

then rseqi is convergent by SEQ_4:58;
hence S₁[i, lim rseqi] 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 Element of NAT st k in Seg n holds
S₁[k,f . k] by A9;
hence vseq is convergent by A10, Th11; :: thesis: verum