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