let X be NormedLinearTopSpace; :: thesis: for V being Subset of X holds
( V is compact iff 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 ) )
let V be Subset of X; :: thesis: ( V is compact iff 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 ) )
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;

hereby :: thesis: ( ( 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 ) ) implies V is compact )

assume A2: V is compact ; :: thesis: 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 )
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 )

proof

let F0 be Subset-Family of (TopSpaceNorm RNS); :: thesis: ( F0 is Cover of V0 & F0 is open implies ex G being Subset-Family of (TopSpaceNorm RNS) st
( G c= F0 & G is Cover of V0 & G is finite ) )
assume A3: ( F0 is Cover of V0 & F0 is open ) ; :: thesis: ex G being Subset-Family of (TopSpaceNorm RNS) st
( G c= F0 & G is Cover of V0 & G is finite )
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

proof

let P be Subset of X; :: thesis: ( P in F implies P is open )
assume A5: P in F ; :: thesis: P is open
reconsider P0 = P as Subset of (TopSpaceNorm RNS) by A1;
P0 is open by A3, TOPS_2:def 1, A5;
hence P is open by A1; :: thesis: verum

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: ( G0 c= F0 & G0 is Cover of V0 & G0 is finite )
thus G0 c= F0 by A6; :: thesis: ( G0 is Cover of V0 & G0 is finite )
thus G0 is Cover of V0 by A6; :: thesis: G0 is finite
thus G0 is finite by A6; :: thesis: verum

end;

then V0 is compact by COMPTS_1:def 4;
then A7: V1 is compact by TOPMETR4:19;
thus 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: verum

proof

let s1 be sequence of X; :: thesis: ( rng s1 c= V implies ex s2 being sequence of X st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in V ) )
reconsider t1 = s1 as sequence of RNS by A1;
assume rng s1 c= V ; :: thesis: ex s2 being sequence of X st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in V )
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: ( s2 is subsequence of s1 & s2 is convergent & lim s2 in V )
thus s2 is subsequence of s1 by A9; :: thesis: ( s2 is convergent & lim s2 in V )
s2 is convergent by A9, Th27, A1;
hence ( s2 is convergent & lim s2 in V ) by A9, A1, Th26; :: thesis: verum

end;

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: V is compact
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 )

proof

let s1 be sequence of RNS; :: thesis: ( rng s1 c= V1 implies ex s2 being sequence of RNS st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in V1 ) )
assume A12: rng s1 c= V1 ; :: thesis: ex s2 being sequence of RNS st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in V1 )
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: ( s2 is subsequence of s1 & s2 is convergent & lim s2 in V1 )
thus s2 is subsequence of s1 by A13; :: thesis: ( s2 is convergent & lim s2 in V1 )
thus ( s2 is convergent & lim s2 in V1 ) by A13, Th26, A1; :: thesis: verum

end;

then V1 is compact ;
then A14: V0 is compact by TOPMETR4:19;
for F being Subset-Family of X st F is Cover of V & F is open holds
ex G being Subset-Family of X st
( G c= F & G is Cover of V & G is finite )

proof

let F be Subset-Family of X; :: thesis: ( F is Cover of V & F is open implies ex G being Subset-Family of X st
( G c= F & G is Cover of V & G is finite ) )
assume A15: ( F is Cover of V & F is open ) ; :: thesis: ex G being Subset-Family of X st
( G c= F & G is Cover of V & G is finite )
reconsider F0 = F as Subset-Family of (TopSpaceNorm RNS) by A1;
A16: for P0 being Subset of (TopSpaceNorm RNS) st P0 in F0 holds
P0 is open

proof

let P0 be Subset of (TopSpaceNorm RNS); :: thesis: ( P0 in F0 implies P0 is open )
assume A17: P0 in F0 ; :: thesis: P0 is open
reconsider P = P0 as Subset of X by A1;
P is open by A15, TOPS_2:def 1, A17;
hence P0 is open by A1; :: thesis: verum

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: ( G c= F & G is Cover of V & G is finite )
thus G c= F by A18; :: thesis: ( G is Cover of V & G is finite )
thus G is Cover of V by A18; :: thesis: G is finite
thus G is finite by A18; :: thesis: verum

end;

hence V is compact by COMPTS_1:def 4; :: thesis: verum