let n, m be non empty Element of NAT ; 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 ; 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); 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); ( 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
; ( 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:40;
hence
f1 + f2 is_partial_differentiable_in x,i
by Def9; 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:40; verum