let F be sequence of 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 that
A1: ex n being Element of NAT st x <= F . n and
A2: F is nonnegative ; :: thesis: x <= SUM F
consider n being Element of NAT such that
A3: x <= F . n by A1;
A4: (Ser F) . n <= SUM F by FUNCT_2:4, XXREAL_2:4;

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:def 11;
hence x <= SUM F by A3, A4, 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
A5: n = k + 1 ;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A6: 0. <= (Ser F) . k by A2, SUPINF_2:40;
(Ser F) . n = ((Ser F) . k) + (F . (k + 1)) by A5, SUPINF_2:def 11;
then 0. + x <= (Ser F) . n by A3, A5, A6, XXREAL_3:36;
then x <= (Ser F) . n by XXREAL_3:4;
hence x <= SUM F by A4, XXREAL_0:2; :: thesis: verum

end;

end;