let X be NormedLinearTopSpace; :: thesis: for RNS being RealNormSpace
for V being Subset of X
for W being Subset of RNS st 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) & V = W holds
( V is compact iff W is compact )
let RNS be RealNormSpace; :: thesis: for V being Subset of X
for W being Subset of RNS st 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) & V = W holds
( V is compact iff W is compact )
let V be Subset of X; :: thesis: for W being Subset of RNS st 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) & V = W holds
( V is compact iff W is compact )
let V0 be Subset of RNS; :: thesis: ( 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) & V = V0 implies ( V is compact iff V0 is compact ) )
assume 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) & V = V0 ) ; :: thesis: ( V is compact iff V0 is compact )

hereby :: thesis: ( V0 is compact implies V is compact )

assume A2: V is compact ; :: thesis: V0 is compact
for t1 being sequence of RNS st rng t1 c= V0 holds
ex t2 being sequence of RNS st
( t2 is subsequence of t1 & t2 is convergent & lim t2 in V0 )

proof

let t1 be sequence of RNS; :: thesis: ( rng t1 c= V0 implies ex t2 being sequence of RNS st
( t2 is subsequence of t1 & t2 is convergent & lim t2 in V0 ) )
assume A3: rng t1 c= V0 ; :: thesis: ex t2 being sequence of RNS st
( t2 is subsequence of t1 & t2 is convergent & lim t2 in V0 )
reconsider s1 = t1 as sequence of X by A1;
consider s2 being sequence of X such that
A4: ( s2 is subsequence of s1 & s2 is convergent & lim s2 in V ) by A2, Th31, A3, A1;
reconsider t2 = s2 as sequence of RNS by A1;
take t2 ; :: thesis: ( t2 is subsequence of t1 & t2 is convergent & lim t2 in V0 )
thus ( t2 is subsequence of t1 & t2 is convergent & lim t2 in V0 ) by A4, A1, Th26; :: thesis: verum

end;

hence V0 is compact ; :: thesis: verum

end;

assume A5: V0 is compact ; :: thesis: V is compact
for t1 being sequence of X st rng t1 c= V holds
ex t2 being sequence of X st
( t2 is subsequence of t1 & t2 is convergent & lim t2 in V )

proof

let t1 be sequence of X; :: thesis: ( rng t1 c= V implies ex t2 being sequence of X st
( t2 is subsequence of t1 & t2 is convergent & lim t2 in V ) )
assume A6: rng t1 c= V ; :: thesis: ex t2 being sequence of X st
( t2 is subsequence of t1 & t2 is convergent & lim t2 in V )
reconsider s1 = t1 as sequence of RNS by A1;
consider s2 being sequence of RNS such that
A7: ( s2 is subsequence of s1 & s2 is convergent & lim s2 in V0 ) by A5, A6, A1;
reconsider t2 = s2 as sequence of X by A1;
take t2 ; :: thesis: ( t2 is subsequence of t1 & t2 is convergent & lim t2 in V )
t2 is convergent by A7, A1, Th27;
hence ( t2 is subsequence of t1 & t2 is convergent & lim t2 in V ) by A7, A1, Th26; :: thesis: verum

end;

hence V is compact by Th31; :: thesis: verum