let seq be Real_Sequence; :: thesis: ( seq is bounded_above & seq is non-decreasing implies for n being Nat holds seq . n <= lim seq )
assume that
A1: seq is bounded_above and
A2: seq is non-decreasing ; :: thesis: for n being Nat holds seq . n <= lim seq
let m be Nat; :: thesis: seq . m <= lim seq
set seq1 = NAT --> (seq . m);
deffunc H₁( Nat) -> Element of REAL = seq . ($1 + m);
consider seq2 being Real_Sequence such that
A3: for n being Nat holds seq2 . n = H₁(n) from SEQ_1:sch 1();

A4: now :: thesis: for n being Nat holds (NAT --> (seq . m)) . n <= seq2 . n

let n be Nat; :: thesis: (NAT --> (seq . m)) . n <= seq2 . n
n in NAT by ORDINAL1:def 12;
then ( (NAT --> (seq . m)) . n = seq . m & seq2 . n = seq . (m + n) ) by A3, FUNCOP_1:7;
hence (NAT --> (seq . m)) . n <= seq2 . n by A2, SEQM_3:5; :: thesis: verum

end;

(NAT --> (seq . m)) . 0 = seq . m ;
then A5: lim (NAT --> (seq . m)) = seq . m by Th25;
for n being Nat holds seq2 . n = H₁(n) by A3;
then A6: seq2 = seq ^\ m by NAT_1:def 3;
then lim seq2 = lim seq by A1, A2, Th17;
hence seq . m <= lim seq by A1, A2, A5, A6, A4, SEQ_2:18; :: thesis: verum