let F be Function of NAT , ExtREAL ; :: thesis: ( F is nonnegative & ex n being Element of NAT st F . n = +infty implies SUM F = +infty )
assume A1: F is nonnegative ; :: thesis: ( for n being Element of NAT holds not F . n = +infty or SUM F = +infty )
given n being Element of NAT such that A2: F . n = +infty ; :: thesis: SUM F = +infty
A3: ( n = 0 implies SUM F = +infty )

proof

assume n = 0 ; :: thesis: SUM F = +infty
then A4: (Ser F) . 0 = +infty by A2, Th63;
reconsider x = (Ser F) . 0 as R_eal ;
x is UpperBound of rng (Ser F) by A4, XXREAL_2:41;
hence SUM F = +infty by A4, FUNCT_2:6, XXREAL_2:55; :: thesis: verum

end;

( ex k being Nat st n = k + 1 implies SUM F = +infty )

proof

given k being Nat such that A5: n = k + 1 ; :: thesis: SUM F = +infty
reconsider k = k as Element of NAT by ORDINAL1:def 13;
A6: (Ser F) . k <> -infty by A1, Th59, XXREAL_0:6;
reconsider y = (Ser F) . k as R_eal ;
A7: (Ser F) . (k + 1) = y + (F . (k + 1)) by Th63;
reconsider x = (Ser F) . (k + 1) as R_eal ;
A8: x = +infty by A2, A5, A6, A7, Def2;
then x is UpperBound of rng (Ser F) by XXREAL_2:41;
hence SUM F = +infty by A8, FUNCT_2:6, XXREAL_2:55; :: thesis: verum

end;

hence SUM F = +infty by A3, NAT_1:6; :: thesis: verum