let NrSp be RealNormSpace; :: thesis:
let S be Subset of NrSp; :: thesis:
let T be Subset of (MetricSpaceNorm NrSp); :: thesis:
assume A1: S = T ; :: thesis:

hereby :: thesis:

assume A2: S is compact ; :: thesis:

now :: thesis:

let S1 be sequence of (MetricSpaceNorm NrSp); :: thesis:
assume A3: rng S1 c= T ; :: thesis:
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:
thus ex N being increasing sequence of NAT st S2 = S1 * N by A5; :: thesis:
thus S2 is convergent by A4, NORMSP_2:5; :: thesis:
hence lim S2 in T by A1, A4, NORMSP_2:6; :: thesis:

end;

hence T is sequentially_compact ; :: thesis:

end;

assume A6: T is sequentially_compact ; :: thesis:

now :: thesis:

let s1 be sequence of NrSp; :: thesis:
assume A7: rng s1 c= S ; :: thesis:
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:
thus s2 is subsequence of s1 by A9; :: thesis:
thus s2 is convergent by A8, NORMSP_2:5; :: thesis:
thus lim s2 in S by A1, A8, NORMSP_2:6; :: thesis:

end;

hence S is compact ; :: thesis: