let F, G, H be Function of NAT ,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 Element of NAT holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n) )
assume A1:
( G is nonnegative & H is nonnegative )
; :: thesis: ( ex n being Element of NAT st not F . n = (G . n) + (H . n) or for n being Element of NAT holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n) )
assume A2:
for n being Element of NAT holds F . n = (G . n) + (H . n)
; :: thesis: for n being Element of NAT holds (Ser F) . n = ((Ser G) . n) + ((Ser H) . n)
defpred S1[ Element of NAT ] means (Ser F) . $1 = ((Ser G) . $1) + ((Ser H) . $1);
( (Ser F) . 0 = F . 0 & (Ser G) . 0 = G . 0 & (Ser H) . 0 = H . 0 )
by SUPINF_2:63;
then A3:
S1[ 0 ]
by A2;
A4:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A5:
(Ser F) . k = ((Ser G) . k) + ((Ser H) . k)
;
:: thesis: S1[k + 1]
A6:
F . (k + 1) = (G . (k + 1)) + (H . (k + 1))
by A2;
A7:
(
(Ser G) . (k + 1) = ((Ser G) . k) + (G . (k + 1)) &
(Ser H) . (k + 1) = ((Ser H) . k) + (H . (k + 1)) )
by SUPINF_2:63;
set n =
k + 1;
(
0. <= G . (k + 1) &
0. <= H . (k + 1) )
by A1, SUPINF_2:58;
then
0. + 0. <= (G . (k + 1)) + (H . (k + 1))
by XXREAL_3:38;
then A8:
0. <= F . (k + 1)
by A2;
A9:
(
0. <= (Ser G) . k &
0. <= (Ser H) . k &
0. <= (Ser G) . (k + 1) )
by A1, SUPINF_2:59;
A10:
(
0. <= H . (k + 1) &
0. <= G . (k + 1) )
by A1, SUPINF_2:58;
(((Ser G) . k) + ((Ser H) . k)) + (F . (k + 1)) =
(((Ser G) . k) + (F . (k + 1))) + ((Ser H) . k)
by A8, A9, XXREAL_3:48
.=
((((Ser G) . k) + (G . (k + 1))) + (H . (k + 1))) + ((Ser H) . k)
by A6, A9, A10, XXREAL_3:48
.=
((Ser G) . (k + 1)) + ((Ser H) . (k + 1))
by A7, A9, A10, XXREAL_3:48
;
hence
S1[
k + 1]
by A5, SUPINF_2:63;
:: thesis: verum
end;
thus
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A3, A4); :: thesis: verum