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