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