let X be NormedLinearTopSpace; :: thesis:
let V be Subset of X; :: thesis:
consider RNS being RealNormSpace such that
A1: ( RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & the topology of X = the topology of (TopSpaceNorm RNS) ) by Def7;
reconsider V0 = V as Subset of (TopSpaceNorm RNS) by A1;
reconsider V1 = V as Subset of RNS by A1;

assume A2: V is compact ; :: thesis:
for F being Subset-Family of (TopSpaceNorm RNS) st F is Cover of V0 & F is open holds
ex G being Subset-Family of (TopSpaceNorm RNS) st
( G c= F & G is Cover of V0 & G is finite )

let F0 be Subset-Family of (TopSpaceNorm RNS); :: thesis:
assume A3: ( F0 is Cover of V0 & F0 is open ) ; :: thesis:
reconsider F = F0 as Subset-Family of X by A1;
A4: for P being Subset of X st P in F holds
P is open

end;

consider G being Subset-Family of X such that
A6: ( G c= F & G is Cover of V & G is finite ) by A2, COMPTS_1:def 4, A3, A4, TOPS_2:def 1;
reconsider G0 = G as Subset-Family of (TopSpaceNorm RNS) by A1;
take G0 ; :: thesis:
thus G0 c= F0 by A6; :: thesis:
thus G0 is Cover of V0 by A6; :: thesis:
thus G0 is finite by A6; :: thesis:

end;

let s1 be sequence of X; :: thesis:
reconsider t1 = s1 as sequence of RNS by A1;
assume rng s1 c= V ; :: thesis:
then consider t2 being sequence of RNS such that
A9: ( t2 is subsequence of t1 & t2 is convergent & lim t2 in V1 ) by A7;
reconsider s2 = t2 as sequence of X by A1;
take s2 ; :: thesis:
thus s2 is subsequence of s1 by A9; :: thesis:
s2 is convergent by A9, Th27, A1;
hence ( s2 is convergent & lim s2 in V ) by A9, A1, Th26; :: thesis:

end;

assume A11: for s1 being sequence of X st rng s1 c= V holds
ex s2 being sequence of X st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in V ) ; :: thesis:
for s1 being sequence of RNS st rng s1 c= V1 holds
ex s2 being sequence of RNS st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in V1 )

let s1 be sequence of RNS; :: thesis:
assume A12: rng s1 c= V1 ; :: thesis:
reconsider t1 = s1 as sequence of X by A1;
consider t2 being sequence of X such that
A13: ( t2 is subsequence of t1 & t2 is convergent & lim t2 in V ) by A11, A12;
reconsider s2 = t2 as sequence of RNS by A1;
take s2 ; :: thesis:
thus s2 is subsequence of s1 by A13; :: thesis:
thus ( s2 is convergent & lim s2 in V1 ) by A13, Th26, A1; :: thesis:

end;

end;

consider G0 being Subset-Family of (TopSpaceNorm RNS) such that
A18: ( G0 c= F0 & G0 is Cover of V0 & G0 is finite ) by A14, COMPTS_1:def 4, A15, A16, TOPS_2:def 1;
reconsider G = G0 as Subset-Family of X by A1;
take G ; :: thesis:
thus G c= F by A18; :: thesis:
thus G is Cover of V by A18; :: thesis:
thus G is finite by A18; :: thesis:

end;