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 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, Def9;
A4: f2 * (reproj (i,x)) is_differentiable_in (Proj (i,m)) . x by A2, 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 A3, A4, 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 A3, A4, NDIFF_1:41; :: thesis: verum