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
f1 - f2 is_differentiable_on n,Z
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
f1 - f2 is_differentiable_on n,Z
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z implies f1 - f2 is_differentiable_on n,Z )
assume that
A1: f1 is_differentiable_on n,Z and
A2: f2 is_differentiable_on n,Z ; :: thesis: f1 - f2 is_differentiable_on n,Z

now

let i be Element of NAT ; :: thesis: ( i <= n - 1 implies (diff ((f1 - f2),Z)) . i is_differentiable_on Z )
assume A3: i <= n - 1 ; :: thesis: (diff ((f1 - f2),Z)) . i is_differentiable_on Z
A4: (diff (f2,Z)) . i is_differentiable_on Z by A2, A3, TAYLOR_1:def 6;
then A5: Z c= dom ((diff (f2,Z)) . i) by FDIFF_1:def 6;
i <= n by A3, WSIERP_1:18;
then A6: (diff ((f1 - f2),Z)) . i = ((diff (f1,Z)) . i) - ((diff (f2,Z)) . i) by A1, A2, Th18;
A7: (diff (f1,Z)) . i is_differentiable_on Z by A1, A3, TAYLOR_1:def 6;
then Z c= dom ((diff (f1,Z)) . i) by FDIFF_1:def 6;
then Z c= (dom ((diff (f1,Z)) . i)) /\ (dom ((diff (f2,Z)) . i)) by A5, XBOOLE_1:19;
then Z c= dom (((diff (f1,Z)) . i) - ((diff (f2,Z)) . i)) by VALUED_1:12;
hence (diff ((f1 - f2),Z)) . i is_differentiable_on Z by A7, A4, A6, FDIFF_1:19; :: thesis: verum

end;

hence f1 - f2 is_differentiable_on n,Z by TAYLOR_1:def 6; :: thesis: verum