let F, G, H be Function of NAT , ExtREAL ; :: thesis: ( ( for n being Element of NAT holds F . n = (G . n) + (H . n) ) & G is nonnegative & H is nonnegative implies SUM F <= (SUM G) + (SUM H) )
assume A1: for n being Element of NAT holds F . n = (G . n) + (H . n) ; :: thesis: ( not G is nonnegative or not H is nonnegative or SUM F <= (SUM G) + (SUM H) )
assume A2: ( G is nonnegative & H is nonnegative ) ; :: thesis: SUM F <= (SUM G) + (SUM H)
defpred S₁[ Element of NAT ] means (Ser F) . $1 = ((Ser G) . $1) + ((Ser H) . $1);
A3: S₁[ 0 ]

proof

( (Ser F) . 0 = F . 0 & (Ser G) . 0 = G . 0 & (Ser H) . 0 = H . 0 ) by SUPINF_2:63;
hence S₁[ 0 ] by A1; :: thesis: verum

end;

A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: (Ser F) . k = ((Ser G) . k) + ((Ser H) . k) ; :: thesis: S₁[k + 1]
A6: ( (Ser F) . (k + 1) = ((Ser F) . k) + (F . (k + 1)) & (Ser G) . (k + 1) = ((Ser G) . k) + (G . (k + 1)) & (Ser H) . (k + 1) = ((Ser H) . k) + (H . (k + 1)) ) by SUPINF_2:63;
( 0. <= G . (k + 1) & 0. <= H . (k + 1) ) by A2, SUPINF_2:58;
then 0. + 0. <= (G . (k + 1)) + (H . (k + 1)) by MEASURE1:4;
then 0. <= (G . (k + 1)) + (H . (k + 1)) by SUPINF_2:18;
then A7: 0. <= F . (k + 1) by A1;
A8: ( 0. <= (Ser G) . k & 0. <= G . (k + 1) & 0. <= (Ser H) . k & 0. <= H . (k + 1) & 0. <= (Ser H) . (k + 1) ) by A2, SUPINF_2:58, SUPINF_2:59;
hence (Ser F) . (k + 1) = ((Ser G) . k) + (((Ser H) . k) + (F . (k + 1))) by A5, A6, A7, MEASURE4:1
.= ((Ser G) . k) + (((Ser H) . k) + ((G . (k + 1)) + (H . (k + 1)))) by A1
.= ((Ser G) . k) + ((((Ser H) . k) + (H . (k + 1))) + (G . (k + 1))) by A8, MEASURE4:1
.= ((Ser G) . (k + 1)) + ((Ser H) . (k + 1)) by A6, A8, MEASURE4:1 ;
:: thesis: verum

end;

A9: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A3, A4);
(SUM G) + (SUM H) is UpperBound of rng (Ser F)

proof

let x be ext-real number ; :: according to XXREAL_2:def 1 :: thesis: ( not x in rng (Ser F) or x <= (SUM G) + (SUM H) )
assume A10: x in rng (Ser F) ; :: thesis: x <= (SUM G) + (SUM H)
dom (Ser F) = NAT by FUNCT_2:def 1;
then consider n being set such that
A11: ( n in NAT & x = (Ser F) . n ) by A10, FUNCT_1:def 5;
reconsider n = n as Element of NAT by A11;
( (Ser G) . n <= sup (rng (Ser G)) & (Ser H) . n <= sup (rng (Ser H)) ) by FUNCT_2:6, XXREAL_2:4;
then A12: ( (Ser G) . n <= SUM G & (Ser H) . n <= SUM H ) by SUPINF_2:def 23;
( 0. <= (Ser G) . n & 0. <= (Ser H) . n ) by A2, SUPINF_2:59;
then ((Ser G) . n) + ((Ser H) . n) <= (SUM G) + (SUM H) by A12, MEASURE1:4;
hence x <= (SUM G) + (SUM H) by A9, A11; :: thesis: verum

end;

then sup (rng (Ser F)) <= (SUM G) + (SUM H) by XXREAL_2:def 3;
hence SUM F <= (SUM G) + (SUM H) by SUPINF_2:def 23; :: thesis: verum