let u0 be Element of REAL 3; :: thesis: for f1, f2 being PartFunc of (REAL 3),REAL st f1 is_hpartial_differentiable`23_in u0 & f2 is_hpartial_differentiable`23_in u0 holds
(pdiff1 f1,2) (#) (pdiff1 f2,2) is_partial_differentiable_in u0,3
let f1, f2 be PartFunc of (REAL 3),REAL ; :: thesis: ( f1 is_hpartial_differentiable`23_in u0 & f2 is_hpartial_differentiable`23_in u0 implies (pdiff1 f1,2) (#) (pdiff1 f2,2) is_partial_differentiable_in u0,3 )
assume ( f1 is_hpartial_differentiable`23_in u0 & f2 is_hpartial_differentiable`23_in u0 ) ; :: thesis: (pdiff1 f1,2) (#) (pdiff1 f2,2) is_partial_differentiable_in u0,3
then ( pdiff1 f1,2 is_partial_differentiable_in u0,3 & pdiff1 f2,2 is_partial_differentiable_in u0,3 ) by Th12ForZ;
hence (pdiff1 f1,2) (#) (pdiff1 f2,2) is_partial_differentiable_in u0,3 by PDIFF_4:30; :: thesis: verum