let NrSp be RealNormSpace; :: thesis: for S being Subset of NrSp
for T being Subset of (MetricSpaceNorm NrSp) st S = T holds
( S is compact iff T is sequentially_compact )
let S be Subset of NrSp; :: thesis: for T being Subset of (MetricSpaceNorm NrSp) st S = T holds
( S is compact iff T is sequentially_compact )
let T be Subset of (MetricSpaceNorm NrSp); :: thesis: ( S = T implies ( S is compact iff T is sequentially_compact ) )
assume A1: S = T ; :: thesis: ( S is compact iff T is sequentially_compact )

hereby :: thesis: ( T is sequentially_compact implies S is compact )

assume A2: S is compact ; :: thesis: T is sequentially_compact

now :: thesis: for S1 being sequence of (MetricSpaceNorm NrSp) st rng S1 c= T holds
ex S2 being sequence of (MetricSpaceNorm NrSp) st
( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in T )

let S1 be sequence of (MetricSpaceNorm NrSp); :: thesis: ( rng S1 c= T implies ex S2 being sequence of (MetricSpaceNorm NrSp) st
( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in T ) )
assume A3: rng S1 c= T ; :: thesis: ex S2 being sequence of (MetricSpaceNorm NrSp) st
( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in T )
reconsider s1 = S1 as sequence of NrSp ;
consider s2 being sequence of NrSp such that
A4: ( s2 is subsequence of s1 & s2 is convergent & lim s2 in S ) by A1, A2, A3;
consider N being increasing sequence of NAT such that
A5: s2 = s1 * N by A4, VALUED_0:def 17;
reconsider S2 = s2 as sequence of (MetricSpaceNorm NrSp) ;
take S2 = S2; :: thesis: ( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in T )
thus ex N being increasing sequence of NAT st S2 = S1 * N by A5; :: thesis: ( S2 is convergent & lim S2 in T )
thus S2 is convergent by A4, NORMSP_2:5; :: thesis: lim S2 in T
hence lim S2 in T by A1, A4, NORMSP_2:6; :: thesis: verum

end;

hence T is sequentially_compact ; :: thesis: verum

end;

assume A6: T is sequentially_compact ; :: thesis: S is compact

now :: thesis: for s1 being sequence of NrSp st rng s1 c= S holds
ex s2 being sequence of NrSp st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in S )

let s1 be sequence of NrSp; :: thesis: ( rng s1 c= S implies ex s2 being sequence of NrSp st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in S ) )
assume A7: rng s1 c= S ; :: thesis: ex s2 being sequence of NrSp st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in S )
reconsider S1 = s1 as sequence of (MetricSpaceNorm NrSp) ;
consider S2 being sequence of (MetricSpaceNorm NrSp) such that
A8: ( ex N being increasing sequence of NAT st S2 = S1 * N & S2 is convergent & lim S2 in T ) by A1, A6, A7;
consider N being increasing sequence of NAT such that
A9: S2 = S1 * N by A8;
reconsider s2 = S2 as sequence of NrSp ;
take s2 = s2; :: thesis: ( s2 is subsequence of s1 & s2 is convergent & lim s2 in S )
thus s2 is subsequence of s1 by A9; :: thesis: ( s2 is convergent & lim s2 in S )
thus s2 is convergent by A8, NORMSP_2:5; :: thesis: lim s2 in S
thus lim s2 in S by A1, A8, NORMSP_2:6; :: thesis: verum

end;

hence S is compact ; :: thesis: verum