let F1, F2 be sequence of ExtREAL; :: thesis: ( F1 is nonnegative & ( for n being Element of NAT holds F1 . n <= F2 . n ) & F2 is summable implies F1 is summable )

assume F1 is nonnegative ; :: thesis: ( ex n being Element of NAT st not F1 . n <= F2 . n or not F2 is summable or F1 is summable )

then A1: 0. <= (Ser F1) . 0 by Th39;

(Ser F1) . 0 <= sup (rng (Ser F1)) by FUNCT_2:4, XXREAL_2:4;

then A2: SUM F1 <> -infty by A1, XXREAL_0:6;

assume A3: for n being Element of NAT holds F1 . n <= F2 . n ; :: thesis: ( not F2 is summable or F1 is summable )

assume F2 is summable ; :: thesis: F1 is summable

then A4: not SUM F1 = +infty by A3, Th42, XXREAL_0:9;

( SUM F1 in REAL or SUM F1 in {-infty,+infty} ) by XBOOLE_0:def 3;

hence F1 is summable by A4, A2, TARSKI:def 2; :: thesis: verum

assume F1 is nonnegative ; :: thesis: ( ex n being Element of NAT st not F1 . n <= F2 . n or not F2 is summable or F1 is summable )

then A1: 0. <= (Ser F1) . 0 by Th39;

(Ser F1) . 0 <= sup (rng (Ser F1)) by FUNCT_2:4, XXREAL_2:4;

then A2: SUM F1 <> -infty by A1, XXREAL_0:6;

assume A3: for n being Element of NAT holds F1 . n <= F2 . n ; :: thesis: ( not F2 is summable or F1 is summable )

assume F2 is summable ; :: thesis: F1 is summable

then A4: not SUM F1 = +infty by A3, Th42, XXREAL_0:9;

( SUM F1 in REAL or SUM F1 in {-infty,+infty} ) by XBOOLE_0:def 3;

hence F1 is summable by A4, A2, TARSKI:def 2; :: thesis: verum