let S be non empty compact TopSpace; :: thesis: for T being non empty MetrSpace st T is complete holds
for H being non empty Subset of (MetricSpace_of_ContinuousFunctions (S,T)) holds
( Cl H is sequentially_compact iff (MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded )
let T be non empty MetrSpace; :: thesis: ( T is complete implies for H being non empty Subset of (MetricSpace_of_ContinuousFunctions (S,T)) holds
( Cl H is sequentially_compact iff (MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded ) )
assume A1: T is complete ; :: thesis: for H being non empty Subset of (MetricSpace_of_ContinuousFunctions (S,T)) holds
( Cl H is sequentially_compact iff (MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded )
set Z = MetricSpace_of_ContinuousFunctions (S,T);
let H be non empty Subset of (MetricSpace_of_ContinuousFunctions (S,T)); :: thesis: ( Cl H is sequentially_compact iff (MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded )
MetricSpace_of_ContinuousFunctions (S,T) is complete by A1, Th13;
then ( (MetricSpace_of_ContinuousFunctions (S,T)) | (Cl H) is totally_bounded iff Cl H is sequentially_compact ) by TOPMETR4:17, Th3;
hence ( Cl H is sequentially_compact iff (MetricSpace_of_ContinuousFunctions (S,T)) | H is totally_bounded ) by Th4; :: thesis: verum