let F be sequence of 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: ( ex k being Nat st n = k + 1 implies SUM F = +infty )
proof
given k being Nat such that A4: n = k + 1 ; :: thesis: SUM F = +infty
reconsider k = k as Element of NAT by ORDINAL1:def 12;
reconsider y = (Ser F) . k as R_eal ;
reconsider x = (Ser F) . (k + 1) as R_eal ;
A5: (Ser F) . (k + 1) = y + (F . (k + 1)) by Def11;
(Ser F) . k <> -infty by A1, Th39, XXREAL_0:6;
then A6: x = +infty by A2, A4, A5, XXREAL_3:def 2;
then x is UpperBound of rng (Ser F) by XXREAL_2:41;
hence SUM F = +infty by A6, FUNCT_2:4, XXREAL_2:55; :: thesis: verum
end;
( n = 0 implies SUM F = +infty )
proof
reconsider x = (Ser F) . 0 as R_eal ;
assume n = 0 ; :: thesis: SUM F = +infty
then A7: (Ser F) . 0 = +infty by A2, Def11;
then x is UpperBound of rng (Ser F) by XXREAL_2:41;
hence SUM F = +infty by A7, FUNCT_2:4, XXREAL_2:55; :: thesis: verum
end;
hence SUM F = +infty by A3, NAT_1:6; :: thesis: verum