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 e = 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 ;

hence lim seq <= e by A1, A5, A4, SEQ_2:18; :: thesis: verum

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 e = 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

lim (seq ^\ k) = lim seq
by A1, SEQ_4:20;let i be Nat; :: thesis: (seq ^\ k) . i <= (seq_const e) . i

A6: (seq ^\ k) . i = seq . (k + i) by NAT_1:def 3;

seq . (k + i) <= e by A3, NAT_1:11;

hence (seq ^\ k) . i <= (seq_const e) . i by A6, SEQ_1:57; :: thesis: verum

end;A6: (seq ^\ k) . i = seq . (k + i) by NAT_1:def 3;

seq . (k + i) <= e by A3, NAT_1:11;

hence (seq ^\ k) . i <= (seq_const e) . i by A6, SEQ_1:57; :: thesis: verum

hence lim seq <= e by A1, A5, A4, SEQ_2:18; :: thesis: verum