let X, Y, W be RealNormSpace; :: thesis: for z being Point of [:X,Y:]
for f1, f2 being PartFunc of [:X,Y:],W st f1 is_partial_differentiable_in`2 z & f2 is_partial_differentiable_in`2 z holds
( f1 + f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 + f2),z) = (partdiff`2 (f1,z)) + (partdiff`2 (f2,z)) & f1 - f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 - f2),z) = (partdiff`2 (f1,z)) - (partdiff`2 (f2,z)) )
let z be Point of [:X,Y:]; :: thesis: for f1, f2 being PartFunc of [:X,Y:],W st f1 is_partial_differentiable_in`2 z & f2 is_partial_differentiable_in`2 z holds
( f1 + f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 + f2),z) = (partdiff`2 (f1,z)) + (partdiff`2 (f2,z)) & f1 - f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 - f2),z) = (partdiff`2 (f1,z)) - (partdiff`2 (f2,z)) )
let f1, f2 be PartFunc of [:X,Y:],W; :: thesis: ( f1 is_partial_differentiable_in`2 z & f2 is_partial_differentiable_in`2 z implies ( f1 + f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 + f2),z) = (partdiff`2 (f1,z)) + (partdiff`2 (f2,z)) & f1 - f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 - f2),z) = (partdiff`2 (f1,z)) - (partdiff`2 (f2,z)) ) )
assume A1: ( f1 is_partial_differentiable_in`2 z & f2 is_partial_differentiable_in`2 z ) ; :: thesis: ( f1 + f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 + f2),z) = (partdiff`2 (f1,z)) + (partdiff`2 (f2,z)) & f1 - f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 - f2),z) = (partdiff`2 (f1,z)) - (partdiff`2 (f2,z)) )
(f1 * (reproj2 z)) + (f2 * (reproj2 z)) is_differentiable_in z `2 by NDIFF_1:35, A1;
hence f1 + f2 is_partial_differentiable_in`2 z by Th26; :: thesis: ( partdiff`2 ((f1 + f2),z) = (partdiff`2 (f1,z)) + (partdiff`2 (f2,z)) & f1 - f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 - f2),z) = (partdiff`2 (f1,z)) - (partdiff`2 (f2,z)) )
thus partdiff`2 ((f1 + f2),z) = diff (((f1 * (reproj2 z)) + (f2 * (reproj2 z))),(z `2)) by Th26
.= (partdiff`2 (f1,z)) + (partdiff`2 (f2,z)) by NDIFF_1:35, A1 ; :: thesis: ( f1 - f2 is_partial_differentiable_in`2 z & partdiff`2 ((f1 - f2),z) = (partdiff`2 (f1,z)) - (partdiff`2 (f2,z)) )
(f1 * (reproj2 z)) - (f2 * (reproj2 z)) is_differentiable_in z `2 by NDIFF_1:36, A1;
hence f1 - f2 is_partial_differentiable_in`2 z by Th26; :: thesis: partdiff`2 ((f1 - f2),z) = (partdiff`2 (f1,z)) - (partdiff`2 (f2,z))
thus partdiff`2 ((f1 - f2),z) = diff (((f1 * (reproj2 z)) - (f2 * (reproj2 z))),(z `2)) by Th26
.= (partdiff`2 (f1,z)) - (partdiff`2 (f2,z)) by NDIFF_1:36, A1 ; :: thesis: verum