let F, G be sequence of ExtREAL; :: thesis: ( ( 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 A1: 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
set y = (Ser G) . n;
dom (Ser G) = NAT by FUNCT_2:def 1;
then ( SUM G = sup (rng (Ser G)) & (Ser G) . n in rng (Ser G) ) by FUNCT_1:def 3;
hence (Ser F) . n <= SUM G by A1, SUPINF_2:42, XXREAL_2:61; :: thesis: verum