let f be PartFunc of REAL,REAL; :: thesis: for a being Real st f is convergent_in-infty & f is non-increasing holds
for x being Real st x in dom f holds
f . x <= lim_in-infty f
let a be Real; :: thesis: ( f is convergent_in-infty & f is non-increasing implies for x being Real st x in dom f holds
f . x <= lim_in-infty f )
assume that
A1: f is convergent_in-infty and
A2: f is non-increasing ; :: thesis: for x being Real st x in dom f holds
f . x <= lim_in-infty f
let x be Real; :: thesis: ( x in dom f implies f . x <= lim_in-infty f )
assume A3: x in dom f ; :: thesis: f . x <= lim_in-infty f

hereby :: thesis: verum

assume A4: f . x > lim_in-infty f ; :: thesis: contradiction
then A5: (f . x) - (lim_in-infty f) > 0 by XREAL_1:50;
set g1 = (f . x) - (lim_in-infty f);
consider r being Real such that
A6: for r1 being Real st r1 < r & r1 in dom f holds
|.((f . r1) - (lim_in-infty f)).| < (f . x) - (lim_in-infty f) by A5, A1, LIMFUNC1:78;
consider R being Real such that
A7: ( R < min (x,r) & R in dom f ) by A1, LIMFUNC1:45;
A8: ( x >= min (x,r) & r >= min (x,r) ) by XXREAL_0:17;
then R < r by A7, XXREAL_0:2;
then A9: |.((f . R) - (lim_in-infty f)).| < (f . x) - (lim_in-infty f) by A6, A7;
x > R by A8, A7, XXREAL_0:2;
then A10: f . x <= f . R by A2, A3, A7, RFUNCT_2:def 4;
then lim_in-infty f < f . R by A4, XXREAL_0:2;
then (f . R) - (lim_in-infty f) > 0 by XREAL_1:50;
then (f . R) - (lim_in-infty f) < (f . x) - (lim_in-infty f) by A9, ABSVALUE:def 1;
hence contradiction by A10, XREAL_1:9; :: thesis: verum

end;