let Z be RealNormSpace; :: thesis: for F being non empty Subset of Z
for H being non empty Subset of (MetricSpaceNorm Z) st Z is complete & H = F & (MetricSpaceNorm Z) | H is totally_bounded holds
( Cl H is sequentially_compact & (MetricSpaceNorm Z) | (Cl H) is compact & Cl F is compact )
let F be non empty Subset of Z; :: thesis: for H being non empty Subset of (MetricSpaceNorm Z) st Z is complete & H = F & (MetricSpaceNorm Z) | H is totally_bounded holds
( Cl H is sequentially_compact & (MetricSpaceNorm Z) | (Cl H) is compact & Cl F is compact )
let H be non empty Subset of (MetricSpaceNorm Z); :: thesis: ( Z is complete & H = F & (MetricSpaceNorm Z) | H is totally_bounded implies ( Cl H is sequentially_compact & (MetricSpaceNorm Z) | (Cl H) is compact & Cl F is compact ) )
set K = Cl H;
set M = MetricSpaceNorm Z;
assume A1: ( Z is complete & H = F & (MetricSpaceNorm Z) | H is totally_bounded ) ; :: thesis: ( Cl H is sequentially_compact & (MetricSpaceNorm Z) | (Cl H) is compact & Cl F is compact )
then A2: Cl H = Cl F by Th1;
(MetricSpaceNorm Z) | (Cl H) is complete by Th7, A1;
then Cl H is sequentially_compact by TOPMETR4:17, A1, Th8;
hence ( Cl H is sequentially_compact & (MetricSpaceNorm Z) | (Cl H) is compact & Cl F is compact ) by TOPMETR4:14, TOPMETR4:18, A2; :: thesis: verum