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