let z0 be Element of REAL 2; :: thesis: for f1, f2 being PartFunc of (REAL 2),REAL st f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 holds
(pdiff1 f1,1) (#) (pdiff1 f2,1) is_partial_differentiable_in z0,1
let f1, f2 be PartFunc of (REAL 2),REAL ; :: thesis: ( f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 implies (pdiff1 f1,1) (#) (pdiff1 f2,1) is_partial_differentiable_in z0,1 )
assume ( f1 is_hpartial_differentiable`11_in z0 & f2 is_hpartial_differentiable`11_in z0 ) ; :: thesis: (pdiff1 f1,1) (#) (pdiff1 f2,1) is_partial_differentiable_in z0,1
then ( pdiff1 f1,1 is_partial_differentiable_in z0,1 & pdiff1 f2,1 is_partial_differentiable_in z0,1 ) by Th9;
hence (pdiff1 f1,1) (#) (pdiff1 f2,1) is_partial_differentiable_in z0,1 by PDIFF_2:19; :: thesis: verum