let s1 be Real_Sequence; :: thesis: for X being Subset of REAL st ( for p being Real st p in X holds
ex r being Real ex n being Nat st
( 0 < r & ( for m being Nat st n < m holds
r < |.((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 st p in X holds
ex r being Real ex n being Nat st
( 0 < r & ( for m being Nat st n < m holds
r < |.((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 st p in X holds
ex r being Real ex n being Nat st
( 0 < r & ( for m being Nat st n < m holds
r < |.((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, n being Nat such that
A6: 0 < r and
A7: for m being Nat st n < m holds
r < |.((s1 . m) - (lim s2)).| by A1, A5;
consider n1 being Nat such that
A8: for m being Nat st n1 <= m holds
|.((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;
reconsider k = (n + 1) + n1 as Element of NAT by ORDINAL1:def 12;
|.(((s1 * NS) . k) - (lim s2)).| < r by A8, A9, NAT_1:11;
then A10: |.((s1 . (NS . k)) - (lim s2)).| < r by FUNCT_2:15;
n + 1 <= k by NAT_1:11;
then A11: n < k by NAT_1:13;
k <= NS . k by SEQM_3:14;
then n < NS . k by A11, XXREAL_0:2;
hence contradiction by A7, A10; :: thesis: verum