let F, G, H be sequence of 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) )
defpred S₁[ Nat] means (Ser F) . $1 = ((Ser G) . $1) + ((Ser H) . $1);
assume that
A2: G is nonnegative and
A3: H is nonnegative ; :: thesis: SUM F <= (SUM G) + (SUM H)
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A5: ( (Ser G) . (k + 1) = ((Ser G) . k) + (G . (k + 1)) & (Ser H) . (k + 1) = ((Ser H) . k) + (H . (k + 1)) ) by SUPINF_2:def 11;
A6: 0. <= (Ser G) . k by A2, SUPINF_2:40;
A7: 0. <= (Ser H) . (k + 1) by A3, SUPINF_2:40;
A8: 0. <= H . (k + 1) by A3, SUPINF_2:39;
A9: 0. <= (Ser H) . k by A3, SUPINF_2:40;
( 0. <= G . (k + 1) & 0. <= H . (k + 1) ) by A2, A3, SUPINF_2:39;
then 0. + 0. <= (G . (k + 1)) + (H . (k + 1)) by XXREAL_3:36;
then A10: ( (Ser F) . (k + 1) = ((Ser F) . k) + (F . (k + 1)) & 0. <= F . (k + 1) ) by A1, SUPINF_2:def 11;
A11: 0. <= G . (k + 1) by A2, SUPINF_2:39;
assume (Ser F) . k = ((Ser G) . k) + ((Ser H) . k) ; :: thesis: S₁[k + 1]
hence (Ser F) . (k + 1) = ((Ser G) . k) + (((Ser H) . k) + (F . (k + 1))) by A10, A6, A9, XXREAL_3:44
.= ((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 A11, A9, A8, XXREAL_3:44
.= ((Ser G) . (k + 1)) + ((Ser H) . (k + 1)) by A5, A6, A11, A7, XXREAL_3:44 ;
:: thesis: verum

end;

A12: (Ser H) . 0 = H . 0 by SUPINF_2:def 11;
( (Ser F) . 0 = F . 0 & (Ser G) . 0 = G . 0 ) by SUPINF_2:def 11;
then A13: S₁[ 0 ] by A1, A12;
A14: for n being Nat holds S₁[n] from NAT_1:sch 2(A13, A4);
(SUM G) + (SUM H) is UpperBound of rng (Ser F)

proof

let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not x in rng (Ser F) or x <= (SUM G) + (SUM H) )
A15: dom (Ser F) = NAT by FUNCT_2:def 1;
assume x in rng (Ser F) ; :: thesis: x <= (SUM G) + (SUM H)
then consider n being object such that
A16: n in NAT and
A17: x = (Ser F) . n by A15, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A16;
(Ser H) . n <= sup (rng (Ser H)) by FUNCT_2:4, XXREAL_2:4;
then A18: (Ser H) . n <= SUM H ;
(Ser G) . n <= sup (rng (Ser G)) by FUNCT_2:4, XXREAL_2:4;
then (Ser G) . n <= SUM G ;
then ((Ser G) . n) + ((Ser H) . n) <= (SUM G) + (SUM H) by A18, XXREAL_3:36;
hence x <= (SUM G) + (SUM H) by A14, A17; :: thesis: verum

end;

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