let r be Real; :: thesis: for seq being Real_Sequence st seq is convergent & lim seq < r holds
ex n being Element of NAT st
for k being Element of NAT st n <= k holds
seq . k < r
let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq < r implies ex n being Element of NAT st
for k being Element of NAT st n <= k holds
seq . k < r )
assume that
A1: seq is convergent and
A2: lim seq < r ; :: thesis: ex n being Element of NAT st
for k being Element of NAT st n <= k holds
seq . k < r
reconsider s = NAT --> r as Real_Sequence ;
A3: s - seq is convergent by A1, SEQ_2:11;
s . 0 = r by FUNCOP_1:7;
then lim s = r by SEQ_4:25;
then lim (s - seq) = r - (lim seq) by A1, SEQ_2:12;
then consider n being Element of NAT such that
A4: for k being Element of NAT st n <= k holds
0 < (s - seq) . k by A2, A3, LIMFUNC1:4, XREAL_1:50;
take n ; :: thesis: for k being Element of NAT st n <= k holds
seq . k < r
let k be Element of NAT ; :: thesis: ( n <= k implies seq . k < r )
assume n <= k ; :: thesis: seq . k < r
then 0 < (s - seq) . k by A4;
then 0 < (s . k) - (seq . k) by RFUNCT_2:1;
then 0 < r - (seq . k) by FUNCOP_1:7;
then 0 + (seq . k) < r by XREAL_1:20;
hence seq . k < r ; :: thesis: verum