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 A1: ( seq is convergent & 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:25;
s . 0 = r by FUNCOP_1:13;
then lim s = r by SEQ_4:40;
then lim (s - seq) = r - (lim seq) by A1, SEQ_2:26;
then 0 < lim (s - seq) by A1, XREAL_1:52;
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 A3, LIMFUNC1:29;
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:6;
then 0 < r - (seq . k) by FUNCOP_1:13;
then 0 + (seq . k) < r by XREAL_1:22;
hence seq . k < r ; :: thesis: verum