let Z be RealNormSpace; :: thesis: for F being non empty Subset of Z
for H being non empty Subset of (MetricSpaceNorm Z)
for T being Subset of (TopSpaceNorm Z) st Z is complete & H = F & H = T holds
( ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl H is sequentially_compact ) & ( Cl H is sequentially_compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies (MetricSpaceNorm Z) | (Cl H) is compact ) & ( (MetricSpaceNorm Z) | (Cl H) is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl F is compact ) & ( Cl F is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl T is compact ) & ( Cl T is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) )
let F be non empty Subset of Z; :: thesis: for H being non empty Subset of (MetricSpaceNorm Z)
for T being Subset of (TopSpaceNorm Z) st Z is complete & H = F & H = T holds
( ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl H is sequentially_compact ) & ( Cl H is sequentially_compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies (MetricSpaceNorm Z) | (Cl H) is compact ) & ( (MetricSpaceNorm Z) | (Cl H) is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl F is compact ) & ( Cl F is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl T is compact ) & ( Cl T is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) )
let H be non empty Subset of (MetricSpaceNorm Z); :: thesis: for T being Subset of (TopSpaceNorm Z) st Z is complete & H = F & H = T holds
( ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl H is sequentially_compact ) & ( Cl H is sequentially_compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies (MetricSpaceNorm Z) | (Cl H) is compact ) & ( (MetricSpaceNorm Z) | (Cl H) is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl F is compact ) & ( Cl F is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl T is compact ) & ( Cl T is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) )
let T be Subset of (TopSpaceNorm Z); :: thesis: ( Z is complete & H = F & H = T implies ( ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl H is sequentially_compact ) & ( Cl H is sequentially_compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies (MetricSpaceNorm Z) | (Cl H) is compact ) & ( (MetricSpaceNorm Z) | (Cl H) is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl F is compact ) & ( Cl F is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl T is compact ) & ( Cl T is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) ) )
assume A1: Z is complete ; :: thesis: ( not H = F or not H = T or ( ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl H is sequentially_compact ) & ( Cl H is sequentially_compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies (MetricSpaceNorm Z) | (Cl H) is compact ) & ( (MetricSpaceNorm Z) | (Cl H) is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl F is compact ) & ( Cl F is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl T is compact ) & ( Cl T is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) ) )
assume A2: ( F = H & H = T ) ; :: thesis: ( ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl H is sequentially_compact ) & ( Cl H is sequentially_compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies (MetricSpaceNorm Z) | (Cl H) is compact ) & ( (MetricSpaceNorm Z) | (Cl H) is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl F is compact ) & ( Cl F is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl T is compact ) & ( Cl T is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) )
then A3: Cl F = Cl H by Th1;
consider HH being Subset of (TopSpaceMetr (MetricSpaceNorm Z)) such that
A4: ( HH = H & Cl H = Cl HH ) by Def1;
(MetricSpaceNorm Z) | (Cl H) is complete by Th7, A1;
hence A5: ( (MetricSpaceNorm Z) | H is totally_bounded iff Cl H is sequentially_compact ) by TOPMETR4:17, Th8; :: thesis: ( ( (MetricSpaceNorm Z) | H is totally_bounded implies (MetricSpaceNorm Z) | (Cl H) is compact ) & ( (MetricSpaceNorm Z) | (Cl H) is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl F is compact ) & ( Cl F is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl T is compact ) & ( Cl T is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) )
thus ( (MetricSpaceNorm Z) | H is totally_bounded iff (MetricSpaceNorm Z) | (Cl H) is compact ) by A5, TOPMETR4:14; :: thesis: ( ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl F is compact ) & ( Cl F is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) & ( (MetricSpaceNorm Z) | H is totally_bounded implies Cl T is compact ) & ( Cl T is compact implies (MetricSpaceNorm Z) | H is totally_bounded ) )
thus ( (MetricSpaceNorm Z) | H is totally_bounded iff Cl F is compact ) by A5, TOPMETR4:18, A3; :: thesis: ( (MetricSpaceNorm Z) | H is totally_bounded iff Cl T is compact )
hence ( (MetricSpaceNorm Z) | H is totally_bounded iff Cl T is compact ) by A3, A2, A4, TOPMETR4:19; :: thesis: verum