let e be Real; :: thesis: for seq being Real_Sequence st seq is convergent & ex k being Nat st
for i being Nat st k <= i holds
seq . i <= e holds
lim seq <= e
let seq be Real_Sequence; :: thesis: ( seq is convergent & ex k being Nat st
for i being Nat st k <= i holds
seq . i <= e implies lim seq <= e )
assume that
A1: seq is convergent and
A2: ex k being Nat st
for i being Nat st k <= i holds
seq . i <= e ; :: thesis: lim seq <= e
consider k being Nat such that
A3: for i being Nat st k <= i holds
seq . i <= e by A2;
reconsider ee = e as Element of REAL by XREAL_0:def 1;
set cseq = seq_const e;
A4: lim (seq_const e) = (seq_const e) . 0 by SEQ_4:26
.= e by SEQ_1:57 ;

A5: now :: thesis: for i being Nat holds (seq ^\ k) . i <= (seq_const e) . i

let i be Nat; :: thesis: (seq ^\ k) . i <= (seq_const e) . i
( (seq ^\ k) . i = seq . (k + i) & seq . (k + i) <= e ) by A3, NAT_1:11, NAT_1:def 3;
hence (seq ^\ k) . i <= (seq_const e) . i by SEQ_1:57; :: 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