let F1, F2 be Function of NAT , ExtREAL ; :: thesis: ( F1 is nonnegative & ( for n being Element of NAT holds F1 . n <= F2 . n ) & F2 is summable implies F1 is summable )
assume A1: 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 )
assume A2: 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 A3: SUM F2 in REAL by Def24;
A4: not SUM F1 = +infty by A3, A2, Th62, XXREAL_0:9;
A5: 0. <= (Ser F1) . 0 by A1, Th59;
(Ser F1) . 0 <= sup (rng (Ser F1)) by FUNCT_2:6, XXREAL_2:4;
then A6: SUM F1 <> -infty by A5, XXREAL_0:2, XXREAL_0:6;
( SUM F1 in REAL or SUM F1 in {-infty ,+infty } ) by XBOOLE_0:def 3;
hence F1 is summable by A4, A6, Def24, TARSKI:def 2; :: thesis: verum