let seq be Real_Sequence; :: thesis: ( seq is bounded_below & seq is non-increasing implies for n being Element of NAT holds lim seq <= seq . n )
assume that
A1: seq is bounded_below and
A2: seq is non-increasing ; :: thesis: for n being Element of NAT holds lim seq <= seq . n
let m be Element of NAT ; :: thesis: lim seq <= seq . m
set seq1 = NAT --> (seq . m);
(NAT --> (seq . m)) . 0 = seq . m by FUNCOP_1:13;
then A7: lim (NAT --> (seq . m)) = seq . m by Th40;
deffunc H₁( Nat) -> Element of REAL = seq . ($1 + m);
consider seq2 being Real_Sequence such that
A8: 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 A8; :: thesis: verum

end;

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

now

let n be Element of NAT ; :: thesis: seq2 . n <= (NAT --> (seq . m)) . n
A12: (NAT --> (seq . m)) . n = seq . m by FUNCOP_1:13;
seq2 . n = seq . (m + n) by A8;
hence seq2 . n <= (NAT --> (seq . m)) . n by A2, A12, SEQM_3:13; :: thesis: verum

end;

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