let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace st T is complete holds
R_NormSpace_of_ContinuousFunctions (S,T) is complete
let T be NormedLinearTopSpace; :: thesis: ( T is complete implies R_NormSpace_of_ContinuousFunctions (S,T) is complete )
set Z = R_NormSpace_of_ContinuousFunctions (S,T);
assume T is complete ; :: thesis: R_NormSpace_of_ContinuousFunctions (S,T) is complete
then for seq being sequence of (R_NormSpace_of_ContinuousFunctions (S,T)) st seq is Cauchy_sequence_by_Norm holds
seq is convergent by Th51;
hence R_NormSpace_of_ContinuousFunctions (S,T) is complete by LOPBAN_1:def 15; :: thesis: verum