let e be Real; :: thesis: for seq being Real_Sequence st seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e holds
lim seq <= e
let seq be Real_Sequence; :: thesis: ( seq is convergent & ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e implies lim seq <= e )
assume that
A1: seq is convergent and
A2: ex k being Element of NAT st
for i being Element of NAT st k <= i holds
seq . i <= e ; :: thesis: lim seq <= e
consider k being Element of NAT such that
A3: for i being Element of NAT st k <= i holds
seq . i <= e by A2;
reconsider cseq = NAT --> e as Real_Sequence ;
A4: lim cseq = cseq . 0 by SEQ_4:26
.= e by FUNCOP_1:7 ;

A5: now

let i be Element of NAT ; :: thesis: (seq ^\ k) . i <= cseq . i
( (seq ^\ k) . i = seq . (k + i) & seq . (k + i) <= e ) by A3, NAT_1:11, NAT_1:def 3;
hence (seq ^\ k) . i <= cseq . i by FUNCOP_1:7; :: thesis: verum

end;

lim (seq ^\ k) = lim seq by A1, SEQ_4:20;
hence lim seq <= e by A1, A5, A4, SEQ_2:18; :: thesis: verum