let n be Element of NAT ; :: thesis: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL ,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds
(diff (f1 + f2),Z) . n = ((diff f1,Z) . n) + ((diff f2,Z) . n)
let Z be open Subset of REAL ; :: thesis: for f1, f2 being PartFunc of REAL ,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds
(diff (f1 + f2),Z) . n = ((diff f1,Z) . n) + ((diff f2,Z) . n)
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z implies (diff (f1 + f2),Z) . n = ((diff f1,Z) . n) + ((diff f2,Z) . n) )
defpred S1[ Nat] means ( f1 is_differentiable_on $1,Z & f2 is_differentiable_on $1,Z implies (diff (f1 + f2),Z) . $1 = ((diff f1,Z) . $1) + ((diff f2,Z) . $1) );
A1:
S1[ 0 ]
proof
assume
(
f1 is_differentiable_on 0 ,
Z &
f2 is_differentiable_on 0 ,
Z )
;
:: thesis: (diff (f1 + f2),Z) . 0 = ((diff f1,Z) . 0 ) + ((diff f2,Z) . 0 )
(diff (f1 + f2),Z) . 0 =
(f1 + f2) | Z
by TAYLOR_1:def 5
.=
(f1 | Z) + (f2 | Z)
by RFUNCT_1:60
.=
((diff f1,Z) . 0 ) + (f2 | Z)
by TAYLOR_1:def 5
.=
((diff f1,Z) . 0 ) + ((diff f2,Z) . 0 )
by TAYLOR_1:def 5
;
hence
(diff (f1 + f2),Z) . 0 = ((diff f1,Z) . 0 ) + ((diff f2,Z) . 0 )
;
:: thesis: verum
end;
A2:
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 A3:
S1[
k]
;
:: thesis: S1[k + 1]
assume A4:
(
f1 is_differentiable_on k + 1,
Z &
f2 is_differentiable_on k + 1,
Z )
;
:: thesis: (diff (f1 + f2),Z) . (k + 1) = ((diff f1,Z) . (k + 1)) + ((diff f2,Z) . (k + 1))
AA:
k < k + 1
by NAT_1:19;
k <= (k + 1) - 1
;
then A8:
(
(diff f1,Z) . k is_differentiable_on Z &
(diff f2,Z) . k is_differentiable_on Z )
by A4, TAYLOR_1:def 6;
(diff (f1 + f2),Z) . (k + 1) =
(((diff f1,Z) . k) + ((diff f2,Z) . k)) `| Z
by A3, AA, A4, TAYLOR_1:23, TAYLOR_1:def 5
.=
(((diff f1,Z) . k) `| Z) + (((diff f2,Z) . k) `| Z)
by A8, FDIFF_2:17
.=
((diff f1,Z) . (k + 1)) + (((diff f2,Z) . k) `| Z)
by TAYLOR_1:def 5
.=
((diff f1,Z) . (k + 1)) + ((diff f2,Z) . (k + 1))
by TAYLOR_1:def 5
;
hence
(diff (f1 + f2),Z) . (k + 1) = ((diff f1,Z) . (k + 1)) + ((diff f2,Z) . (k + 1))
;
:: thesis: verum
end;
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A1, A2);
hence
( f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z implies (diff (f1 + f2),Z) . n = ((diff f1,Z) . n) + ((diff f2,Z) . n) )
; :: thesis: verum