let F be Function of NAT , ExtREAL ; :: thesis: for x being R_eal st ex n being Element of NAT st x <= F . n & F is nonnegative holds
x <= SUM F
let x be R_eal; :: thesis: ( ex n being Element of NAT st x <= F . n & F is nonnegative implies x <= SUM F )
assume A1: ( ex n being Element of NAT st x <= F . n & F is nonnegative ) ; :: thesis: x <= SUM F
then consider n being Element of NAT such that
A2: x <= F . n ;
(Ser F) . n <= sup (rng (Ser F)) by FUNCT_2:6, XXREAL_2:4;
then A3: (Ser F) . n <= SUM F ;

per cases ( n = 0 or ex k being Nat st n = k + 1 ) by NAT_1:6;

suppose n = 0 ; :: thesis: x <= SUM F

then (Ser F) . n = F . n by SUPINF_2:63;
hence x <= SUM F by A2, A3, XXREAL_0:2; :: thesis: verum

end;

suppose ex k being Nat st n = k + 1 ; :: thesis: x <= SUM F

then consider k being Nat such that
A4: n = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A5: (Ser F) . n = ((Ser F) . k) + (F . (k + 1)) by A4, SUPINF_2:63;
( 0. <= (Ser F) . k & x <= F . n & 0. <= F . n ) by A1, A2, SUPINF_2:58, SUPINF_2:59;
then ( not ( 0. = +infty & x = -infty ) & not ( 0. = -infty & x = +infty ) & not ( (Ser F) . k = +infty & F . n = -infty ) & not ( (Ser F) . k = -infty & F . n = +infty ) & 0 <= (Ser F) . k & x <= F . n ) by XXREAL_0:12;
then 0. + x <= (Ser F) . n by A4, A5, SUPINF_2:14;
then x <= (Ser F) . n by SUPINF_2:18;
hence x <= SUM F by A3, XXREAL_0:2; :: thesis: verum

end;

end;