let S be non empty compact TopSpace; :: thesis: for T being NormedLinearTopSpace st T is complete holds
for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st H = F holds
( Cl F is compact iff (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded )
let T be NormedLinearTopSpace; :: thesis: ( T is complete implies for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st H = F holds
( Cl F is compact iff (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded ) )
assume A1: T is complete ; :: thesis: for F being non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T))
for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st H = F holds
( Cl F is compact iff (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded )
set Z = R_NormSpace_of_ContinuousFunctions (S,T);
let F be non empty Subset of (R_NormSpace_of_ContinuousFunctions (S,T)); :: thesis: for H being non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) st H = F holds
( Cl F is compact iff (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded )
let H be non empty Subset of (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))); :: thesis: ( H = F implies ( Cl F is compact iff (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded ) )
assume F = H ; :: thesis: ( Cl F is compact iff (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded )
then A3: Cl F = Cl H by Th1;
( Cl H is sequentially_compact iff (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded ) by Th11, A1;
hence ( Cl F is compact iff (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded ) by TOPMETR4:18, A3; :: thesis: verum