let F, G be Function of NAT ,ExtREAL ; :: thesis: ( F is nonnegative & ( for n being Element of NAT holds F . n <= G . n ) implies for n being Element of NAT holds (Ser F) . n <= SUM G )
assume that
F is nonnegative and
A2: for n being Element of NAT holds F . n <= G . n ; :: thesis: for n being Element of NAT holds (Ser F) . n <= SUM G
let n be Element of NAT ; :: thesis: (Ser F) . n <= SUM G
A3: SUM G = sup (rng (Ser G)) by SUPINF_2:def 23;
set y = (Ser G) . n;
( dom (Ser G) = NAT & rng (Ser G) c= ExtREAL ) by FUNCT_2:def 1;
then ( (Ser G) . n in rng (Ser G) & (Ser F) . n <= (Ser G) . n ) by A2, FUNCT_1:def 5, SUPINF_2:61;
hence (Ser F) . n <= SUM G by A3, XXREAL_2:61; :: thesis: verum