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

now

let n be Nat; :: thesis: seq2 . n = H₁(n)
n in NAT by ORDINAL1:def 13;
hence seq2 . n = H₁(n) by A6; :: thesis: verum

end;

then A7: seq2 = seq ^\ m by NAT_1:def 3;
then A8: lim seq2 = lim seq by A1, A2, Th33;

now

let n be Element of NAT ; :: thesis: seq1 . n <= seq2 . n
A10: seq1 . n = seq . m by FUNCOP_1:13;
seq2 . n = seq . (m + n) by A6;
hence seq1 . n <= seq2 . n by A2, A10, SEQM_3:11; :: thesis: verum

end;

hence seq . m <= lim seq by A5, A8, A1, A2, A7, SEQ_2:32; :: thesis: verum