let F, G, H be sequence of ExtREAL; :: thesis: ( G is nonnegative & H is nonnegative & ( for n being Element of NAT holds F . n = (G . n) + (H . n) ) implies for n being Nat holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n) )
assume that
A1: G is nonnegative and
A2: H is nonnegative ; :: thesis: ( ex n being Element of NAT st not F . n = (G . n) + (H . n) or for n being Nat holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n) )
defpred S₁[ Nat] means (Ser F) . $1 = ((Ser G) . $1) + ((Ser H) . $1);
assume A3: for n being Element of NAT holds F . n = (G . n) + (H . n) ; :: thesis: for n being Nat holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n)
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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