let f be PartFunc of REAL,REAL; :: thesis: for a being Real st f is convergent_in+infty & f is non-decreasing 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-decreasing 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-decreasing ; :: 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 r < r1 & r1 in dom f holds
|.((f . r1) - (lim_in+infty f)).| < (f . x) - (lim_in+infty f) by A5, A1, LIMFUNC1:79;
consider R being Real such that
A7: ( max (x,r) < R & R in dom f ) by A1, LIMFUNC1:44;
A8: ( x <= max (x,r) & r <= max (x,r) ) by XXREAL_0:25;
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 3;
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;