let z0 be Element of REAL 2; :: thesis: for f1, f2 being PartFunc of REAL 2, REAL st f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 holds
(pdiff1 f1,z0) (#) (pdiff1 f2,z0) is_partial_differentiable`2_in z0
let f1, f2 be PartFunc of REAL 2, REAL ; :: thesis: ( f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 implies (pdiff1 f1,z0) (#) (pdiff1 f2,z0) is_partial_differentiable`2_in z0 )
assume ( f1 is_hpartial_differentiable`12_in z0 & f2 is_hpartial_differentiable`12_in z0 ) ; :: thesis: (pdiff1 f1,z0) (#) (pdiff1 f2,z0) is_partial_differentiable`2_in z0
then ( pdiff1 f1,z0 is_partial_differentiable`2_in z0 & pdiff1 f2,z0 is_partial_differentiable`2_in z0 ) by Th10;
hence (pdiff1 f1,z0) (#) (pdiff1 f2,z0) is_partial_differentiable`2_in z0 by PDIFF_2:24; :: thesis: verum