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 and
A4: s2 is convergent and
A5: lim s2 in X by A2;
consider r being real number , n being Element of NAT such that
A6: 0 < r and
A7: for m being Element of NAT st n < m holds
r < abs ((s1 . m) - (lim s2)) by A1, A5;
consider n1 being Element of NAT such that
A8: for m being Element of NAT st n1 <= m holds
abs ((s2 . m) - (lim s2)) < r by A4, A6, SEQ_2:def 7;
consider NS being increasing sequence of NAT such that
A9: s2 = s1 * NS by A3, VALUED_0:def 17;
set k = (n + 1) + n1;
abs (((s1 * NS) . ((n + 1) + n1)) - (lim s2)) < r by A8, A9, NAT_1:11;
then A10: abs ((s1 . (NS . ((n + 1) + n1))) - (lim s2)) < r by FUNCT_2:15;
n + 1 <= (n + 1) + n1 by NAT_1:11;
then A11: n < (n + 1) + n1 by NAT_1:13;
(n + 1) + n1 <= NS . ((n + 1) + n1) by SEQM_3:14;
then n < NS . ((n + 1) + n1) by A11, XXREAL_0:2;
hence contradiction by A7, A10; :: thesis: verum