let m, n be non zero Nat; :: thesis: for i being 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 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 that
A1: f1 is_partial_differentiable_in x,i and
A2: 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)) )
A3: f1 * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A1;
A4: f2 * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A2;
(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 A3, A4, NDIFF_1:36;
hence f1 - f2 is_partial_differentiable_in x,i ; :: 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 A3, A4, NDIFF_1:36; :: thesis: verum