let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace st T is complete holds
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) holds
( Cl H is sequentially_compact iff (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded )
let T be NormedLinearTopSpace; :: thesis: ( T is complete implies for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) holds
( Cl H is sequentially_compact iff (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded ) )
assume A1: T is complete ; :: thesis: for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) holds
( Cl H is sequentially_compact iff (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded )
set Z = R_NormSpace_of_ContinuousFunctions (S,T);
let H be non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))); :: thesis: ( Cl H is sequentially_compact iff (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded )
reconsider F = H as non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T)) ;
set N = (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H;
R_NormSpace_of_ContinuousFunctions (S,T) is complete by A1, C0SP3:52;
then ( (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | (Cl H) is totally_bounded iff Cl H is sequentially_compact ) by TOPMETR4:17, Th7;
hence ( Cl H is sequentially_compact iff (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded ) by Th8; :: thesis: verum