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 S₁[ Element of 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: 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 A2: S₁[k] ; :: thesis: S₁[k + 1]
assume A3: ( 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))
k <= (k + 1) - 1 ;
then A4: ( (diff f1,Z) . k is_differentiable_on Z & (diff f2,Z) . k is_differentiable_on Z ) by A3, TAYLOR_1:def 6;
k < k + 1 by NAT_1:19;
then (diff (f1 - f2),Z) . (k + 1) = (((diff f1,Z) . k) - ((diff f2,Z) . k)) `| Z by A2, A3, TAYLOR_1:23, TAYLOR_1:def 5
.= (((diff f1,Z) . k) `| Z) - (((diff f2,Z) . k) `| Z) by A4, FDIFF_2:18
.= ((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;

A5: S₁[ 0 ]

proof

assume that
f1 is_differentiable_on 0 ,Z and
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:63
.= ((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;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A5, A1);
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