let F be Function of NAT ,ExtREAL ; :: thesis: ( F is nonnegative & SUM F < +infty implies for n being Element of NAT holds F . n in REAL )
assume A1: ( F is nonnegative & SUM F < +infty ) ; :: thesis: for n being Element of NAT holds F . n in REAL
defpred S₁[ Element of NAT ] means F . $1 <= (Ser F) . $1;
A2: S₁[ 0 ] by SUPINF_2:63;
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume F . k <= (Ser F) . k ; :: thesis: S₁[k + 1]
reconsider x = (Ser F) . k, y = F . (k + 1), z = (Ser F) . (k + 1) as R_eal ;
A4: x + (F . (k + 1)) = (Ser F) . (k + 1) by SUPINF_2:63;
( 0. <= x & 0. <= y & 0. <= z ) by A1, SUPINF_2:58, SUPINF_2:59;
hence S₁[k + 1] by A4, XXREAL_3:42; :: thesis: verum

end;

A5: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A3);
let n be Element of NAT ; :: thesis: F . n in REAL
A7: 0. = 0 ;
( F . n <= (Ser F) . n & (Ser F) . n <= SUM F ) by A5, FUNCT_2:6, XXREAL_2:4;
then F . n <= SUM F by XXREAL_0:2;
then ( 0. <= F . n & F . n < +infty ) by A1, SUPINF_2:58, XXREAL_0:2;
hence F . n in REAL by A7, XXREAL_0:46; :: thesis: verum