let n, m be non empty Element of NAT ; :: thesis: for i being Element of NAT
for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds
( f1 - f2 is_partial_differentiable_in x,i & partdiff (f1 - f2),x,i = (partdiff f1,x,i) - (partdiff f2,x,i) )
let i be Element of NAT ; :: thesis: for f1, f2 being PartFunc of (REAL-NS m),(REAL-NS n)
for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds
( f1 - f2 is_partial_differentiable_in x,i & partdiff (f1 - f2),x,i = (partdiff f1,x,i) - (partdiff f2,x,i) )
let f1, f2 be PartFunc of (REAL-NS m),(REAL-NS n); :: thesis: for x being Point of (REAL-NS m) st f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i holds
( f1 - f2 is_partial_differentiable_in x,i & partdiff (f1 - f2),x,i = (partdiff f1,x,i) - (partdiff f2,x,i) )
let x be Point of (REAL-NS m); :: thesis: ( f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i implies ( f1 - f2 is_partial_differentiable_in x,i & partdiff (f1 - f2),x,i = (partdiff f1,x,i) - (partdiff f2,x,i) ) )
assume ( f1 is_partial_differentiable_in x,i & f2 is_partial_differentiable_in x,i ) ; :: thesis: ( f1 - f2 is_partial_differentiable_in x,i & partdiff (f1 - f2),x,i = (partdiff f1,x,i) - (partdiff f2,x,i) )
then A1: ( f1 * (reproj i,x) is_differentiable_in (Proj i,m) . x & f2 * (reproj i,x) is_differentiable_in (Proj i,m) . x ) by Def9;
(f1 - f2) * (reproj i,x) = (f1 * (reproj i,x)) - (f2 * (reproj i,x)) by Th26;
then (f1 - f2) * (reproj i,x) is_differentiable_in (Proj i,m) . x by A1, NDIFF_1:41;
hence f1 - f2 is_partial_differentiable_in x,i by Def9; :: thesis: partdiff (f1 - f2),x,i = (partdiff f1,x,i) - (partdiff f2,x,i)
diff ((f1 * (reproj i,x)) - (f2 * (reproj i,x))),((Proj i,m) . x) = partdiff (f1 - f2),x,i by Th26;
hence partdiff (f1 - f2),x,i = (partdiff f1,x,i) - (partdiff f2,x,i) by A1, NDIFF_1:41; :: thesis: verum