let s1 be Real_Sequence; :: thesis: for X being Subset of REAL st ( for p being real number st p in X holds
ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((s1 . m) - p) ) ) ) holds
for s2 being Real_Sequence st s2 is subsequence of s1 & s2 is convergent holds
not lim s2 in X
let X be Subset of REAL ; :: thesis: ( ( for p being real number st p in X holds
ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((s1 . m) - p) ) ) ) implies for s2 being Real_Sequence st s2 is subsequence of s1 & s2 is convergent holds
not lim s2 in X )
assume that
A1: for p being real number st p in X holds
ex r being real number ex n being Element of NAT st
( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((s1 . m) - p) ) ) and
A2: ex s2 being Real_Sequence st
( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) ; :: thesis: contradiction
consider s2 being Real_Sequence such that
A3: ( s2 is subsequence of s1 & s2 is convergent & lim s2 in X ) by A2;
consider r being real number , n being Element of NAT such that
A4: ( 0 < r & ( for m being Element of NAT st n < m holds
r < abs ((s1 . m) - (lim s2)) ) ) by A1, A3;
consider n1 being Element of NAT such that
A5: for m being Element of NAT st n1 <= m holds
abs ((s2 . m) - (lim s2)) < r by A3, A4, SEQ_2:def 7;
set k = (n + 1) + n1;
n + 1 <= (n + 1) + n1 by NAT_1:11;
then A6: n < (n + 1) + n1 by NAT_1:13;
consider NS being increasing sequence of NAT such that
A7: s2 = s1 * NS by A3, VALUED_0:def 17;
abs (((s1 * NS) . ((n + 1) + n1)) - (lim s2)) < r by A5, A7, NAT_1:11;
then A8: abs ((s1 . (NS . ((n + 1) + n1))) - (lim s2)) < r by FUNCT_2:21;
(n + 1) + n1 <= NS . ((n + 1) + n1) by SEQM_3:33;
then n < NS . ((n + 1) + n1) by A6, XXREAL_0:2;
hence contradiction by A4, A8; :: thesis: verum