let m be non zero Element of NAT ; :: thesis: for X being Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL m),(REAL 1) st <>* f = g & X c= dom f & f is_differentiable_on X holds
( g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
(f `| X) /. x = (proj (1,1)) * ((g `| X) /. x) ) )
let X be Subset of (REAL m); :: thesis: for f being PartFunc of (REAL m),REAL
for g being PartFunc of (REAL m),(REAL 1) st <>* f = g & X c= dom f & f is_differentiable_on X holds
( g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
(f `| X) /. x = (proj (1,1)) * ((g `| X) /. x) ) )
let f be PartFunc of (REAL m),REAL; :: thesis: for g being PartFunc of (REAL m),(REAL 1) st <>* f = g & X c= dom f & f is_differentiable_on X holds
( g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
(f `| X) /. x = (proj (1,1)) * ((g `| X) /. x) ) )
let g be PartFunc of (REAL m),(REAL 1); :: thesis: ( <>* f = g & X c= dom f & f is_differentiable_on X implies ( g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
(f `| X) /. x = (proj (1,1)) * ((g `| X) /. x) ) ) )
assume A1: ( <>* f = g & X c= dom f & f is_differentiable_on X ) ; :: thesis: ( g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
(f `| X) /. x = (proj (1,1)) * ((g `| X) /. x) ) )
hence g is_differentiable_on X by Th53; :: thesis: for x being Element of REAL m st x in X holds
(f `| X) /. x = (proj (1,1)) * ((g `| X) /. x)
A2: dom f = dom (<>* f) by Th3;
let x be Element of REAL m; :: thesis: ( x in X implies (f `| X) /. x = (proj (1,1)) * ((g `| X) /. x) )
assume A3: x in X ; :: thesis: (f `| X) /. x = (proj (1,1)) * ((g `| X) /. x)
then (f `| X) /. x = diff (f,x) by A1, Def4;
hence (f `| X) /. x = (proj (1,1)) * ((g `| X) /. x) by A2, A1, A3, Def1; :: thesis: verum