let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace st T is complete holds
for seq being sequence of (R_NormSpace_of_ContinuousFunctions (S,T)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
let T be NormedLinearTopSpace; :: thesis: ( T is complete implies for seq being sequence of (R_NormSpace_of_ContinuousFunctions (S,T)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent )
assume A1: T is complete ; :: thesis: for seq being sequence of (R_NormSpace_of_ContinuousFunctions (S,T)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent
set Z = R_NormSpace_of_ContinuousFunctions (S,T);
let vseq be sequence of (R_NormSpace_of_ContinuousFunctions (S,T)); :: thesis: ( vseq is Cauchy_sequence_by_Norm implies vseq is convergent )
assume A2: vseq is Cauchy_sequence_by_Norm ; :: thesis: vseq is convergent
A3: for x being object st x in ContinuousFunctions (S,T) holds
x in BoundedFunctions ( the carrier of S,T) by Th34;
rng vseq c= BoundedFunctions ( the carrier of S,T) by Th34;
then reconsider vseq1 = vseq as sequence of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) by FUNCT_2:6;
A4: 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 e > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((vseq1 . n) - (vseq1 . m)).|| < e
then consider k being Nat such that
A6: for n, m being Nat st n >= k & m >= k holds
||.((vseq . n) - (vseq . m)).|| < e by A2, RSSPACE3:8;
take k = k; :: 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 A6;
hence ||.((vseq1 . n) - (vseq1 . m)).|| < e by Th47, Th36; :: thesis: verum
end;
then A7: vseq1 is Cauchy_sequence_by_Norm by RSSPACE3:8;
A8: vseq1 is convergent by A1, RSSPACE4:25, A4, RSSPACE3:8;
reconsider Y = ContinuousFunctions (S,T) as Subset of (R_NormSpace_of_BoundedFunctions ( the carrier of S,T)) by A3, TARSKI:def 3;
A9: rng vseq c= Y ;
Y is closed by Th50;
then reconsider tv = lim vseq1 as Point of (R_NormSpace_of_ContinuousFunctions (S,T)) by A1, A9, A7, C0SP2:20;
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
A10: for n being Nat st n >= k holds
||.((vseq1 . n) - (lim vseq1)).|| < e by A8, 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 A10;
hence ||.((vseq . n) - tv).|| < e by Th47, Th36; :: thesis: verum
end;
hence for n being Nat st n >= k holds
||.((vseq . n) - tv).|| < e ; :: thesis: verum
end;
hence vseq is convergent ; :: thesis: verum