let I be closed_interval Subset of REAL; :: thesis: for E being Subset of RNS_Real st I = E holds
E is compact
let E be Subset of RNS_Real; :: thesis: ( I = E implies E is compact )
assume A1: I = E ; :: thesis: E is compact
for s1 being sequence of RNS_Real st rng s1 c= E holds
ex s2 being sequence of RNS_Real st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in E )

proof

let s1 be sequence of RNS_Real; :: thesis: ( rng s1 c= E implies ex s2 being sequence of RNS_Real st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in E ) )
assume A2: rng s1 c= E ; :: thesis: ex s2 being sequence of RNS_Real st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in E )
reconsider t1 = s1 as Real_Sequence ;
consider t2 being Real_Sequence such that
A3: ( t2 is subsequence of t1 & t2 is convergent & lim t2 in I ) by A1, A2, RCOMP_1:def 3;
consider N1 being increasing sequence of NAT such that
A4: t2 = t1 * N1 by A3, VALUED_0:def 17;
reconsider s2 = s1 * N1 as sequence of RNS_Real ;
take s2 ; :: thesis: ( s2 is subsequence of s1 & s2 is convergent & lim s2 in E )
thus s2 is subsequence of s1 ; :: thesis: ( s2 is convergent & lim s2 in E )
reconsider s0 = lim t2 as Point of RNS_Real by XREAL_0:def 1;

A5: now :: thesis: for r being Real st 0 < r holds
ex n being Nat st
for m being Nat st n <= m holds
||.((s2 . m) - s0).|| < r

let r be Real; :: thesis: ( 0 < r implies ex n being Nat st
for m being Nat st n <= m holds
||.((s2 . m) - s0).|| < r )
assume 0 < r ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.((s2 . m) - s0).|| < r
then consider n being Nat such that
A6: for m being Nat st n <= m holds
|.((t2 . m) - (lim t2)).| < r by A3, SEQ_2:def 7;
take n = n; :: thesis: for m being Nat st n <= m holds
||.((s2 . m) - s0).|| < r
let m be Nat; :: thesis: ( n <= m implies ||.((s2 . m) - s0).|| < r )
assume n <= m ; :: thesis: ||.((s2 . m) - s0).|| < r
then A7: |.((t2 . m) - (lim t2)).| < r by A6;
(t2 . m) - (lim t2) = (s2 . m) - s0 by A4, DUALSP03:4;
hence ||.((s2 . m) - s0).|| < r by A7, EUCLID:def 2; :: thesis: verum

end;

hence s2 is convergent ; :: thesis: lim s2 in E
hence lim s2 in E by A1, A3, A5, NORMSP_1:def 7; :: thesis: verum

end;

hence E is compact ; :: thesis: verum