let S be non empty compact TopSpace; 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; ( 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
; 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)); 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))); ( H = F implies ( Cl F is compact iff (MetricSpaceNorm (R_NormSpace_of_ContinuousFunctions (S,T))) | H is totally_bounded ) )
assume
F = H
; ( 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; verum