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

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume F . k <= (Ser F) . k ; :: thesis: S₁[k + 1]
reconsider x = (Ser F) . k as R_eal ;
x + (F . (k + 1)) = (Ser F) . (k + 1) by SUPINF_2:def 11;
hence S₁[k + 1] by A1, SUPINF_2:40, XXREAL_3:39; :: thesis: verum

end;

A4: S₁[ 0 ] by SUPINF_2:def 11;
for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A3);
then A5: F . n <= (Ser F) . n ;
(Ser F) . n <= SUM F by FUNCT_2:4, XXREAL_2:4;
then F . n <= SUM F by A5, XXREAL_0:2;
then A6: F . n < +infty by A2, XXREAL_0:2;
A7: 0 in REAL by XREAL_0:def 1;
( 0. = 0 & 0. <= F . n ) by A1, SUPINF_2:39;
hence F . n in REAL by A6, XXREAL_0:46, A7; :: thesis: verum