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,1 holds
SVF1 1,f,u is_differentiable_in x
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,1 holds
SVF1 1,f,u is_differentiable_in x
let f be PartFunc of (REAL 3),REAL ; :: thesis: ( u = <*x,y,z*> & f is_partial_differentiable_in u,1 implies SVF1 1,f,u is_differentiable_in x )
assume that
A1: u = <*x,y,z*> and
A2: f is_partial_differentiable_in u,1 ; :: thesis: SVF1 1,f,u is_differentiable_in x
(proj 1,3) . u = x by A1, Th1;
hence SVF1 1,f,u is_differentiable_in x by A2, PDIFF_1:def 11; :: thesis: verum