let X be non empty closed_interval Subset of REAL; :: thesis: for Y being RealNormSpace
for seq being sequence of (R_NormSpace_of_ContinuousFunctions (X,Y)) st Y is complete & seq is Cauchy_sequence_by_Norm holds
seq is convergent
let Y be RealNormSpace; :: thesis: for seq being sequence of (R_NormSpace_of_ContinuousFunctions (X,Y)) st Y is complete & seq is Cauchy_sequence_by_Norm holds
seq is convergent
let vseq be sequence of (R_NormSpace_of_ContinuousFunctions (X,Y)); :: thesis: ( Y is complete & vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A1: ( Y is complete & vseq is Cauchy_sequence_by_Norm ) ; :: thesis: vseq is convergent
rng vseq c= BoundedFunctions (X,Y) by XBOOLE_1:1;
then reconsider vseq1 = vseq as sequence of (R_NormSpace_of_BoundedFunctions (X,Y)) by FUNCT_2:6;

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

let e be Real; :: thesis: ( e > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e )
assume A2: e > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e
consider k being Nat such that
A3: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A1, A2, RSSPACE3:8;
take k = k; :: thesis: for n, m being Nat st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e

now :: thesis: for n, m being Nat st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e

let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((vseq1 . n) - (vseq1 . m)).|| < e )
assume ( n >= k & m >= k ) ; :: thesis: ||.((vseq1 . n) - (vseq1 . m)).|| < e
then ||.((vseq . n) - (vseq . m)).|| < e by A3;
hence ||.((vseq1 . n) - (vseq1 . m)).|| < e by Th17, Th21; :: thesis: verum

end;

hence for n, m being Nat st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e ; :: thesis: verum

end;

then A4: vseq1 is convergent by A1, LOPBAN_1:def 15, RSSPACE3:8;
reconsider Z = ContinuousFunctions (X,Y) as Subset of (R_NormSpace_of_BoundedFunctions (X,Y)) ;
rng vseq c= ContinuousFunctions (X,Y) ;
then reconsider tv = lim vseq1 as Point of (R_NormSpace_of_ContinuousFunctions (X,Y)) by A4, NFCONT_1:def 3, Th22;
for e being Real st e > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| < e

proof

let e be Real; :: thesis: ( e > 0 implies ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| < e )
assume e > 0 ; :: thesis: ex k being Nat st
for n being Nat st n >= k holds
||.((vseq . n) - tv).|| < e
then consider k being Nat such that
A5: for n being Nat st n >= k holds
||.((vseq1 . n) - (lim vseq1)).|| < e by A4, NORMSP_1:def 7;
take k ; :: thesis: for n being Nat st n >= k holds
||.((vseq . n) - tv).|| < e

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

let n be Nat; :: thesis: ( n >= k implies ||.((vseq . n) - tv).|| < e )
assume n >= k ; :: thesis: ||.((vseq . n) - tv).|| < e
then ||.((vseq1 . n) - (lim vseq1)).|| < e by A5;
hence ||.((vseq . n) - tv).|| < e by Th17, Th21; :: thesis: verum

end;

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

end;

hence vseq is convergent by NORMSP_1:def 6; :: thesis: verum