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