let x, y, z be Real; :: thesis: for u being Element of REAL 3
for f being PartFunc of (REAL 3),REAL st u = <*x,y,z*> & f is_partial_differentiable_in u,2 holds
SVF1 2,f,u is_differentiable_in y
let u be Element of REAL 3; :: thesis: for f being PartFunc of (REAL 3),REAL st u = <*x,y,z*> & f is_partial_differentiable_in u,2 holds
SVF1 2,f,u is_differentiable_in y
let f be PartFunc of (REAL 3),REAL ; :: thesis: ( u = <*x,y,z*> & f is_partial_differentiable_in u,2 implies SVF1 2,f,u is_differentiable_in y )
assume that
A1: u = <*x,y,z*> and
A2: f is_partial_differentiable_in u,2 ; :: thesis: SVF1 2,f,u is_differentiable_in y
(proj 2,3) . u = y by A1, Th2;
hence SVF1 2,f,u is_differentiable_in y by A2, PDIFF_1:def 11; :: thesis: verum