let m be non empty 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 AS: ( <>* 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 YTh30; :: thesis: for x being Element of REAL m st x in X holds
(f `| X) /. x = (proj (1,1)) * ((g `| X) /. x)
AA: dom f = dom (<>* f) by LMXTh0;
let x be Element of REAL m; :: thesis: ( x in X implies (f `| X) /. x = (proj (1,1)) * ((g `| X) /. x) )
assume P4: x in X ; :: thesis: (f `| X) /. x = (proj (1,1)) * ((g `| X) /. x)
then (f `| X) /. x = diff (f,x) by AS, XDef1;
hence (f `| X) /. x = (proj (1,1)) * ((g `| X) /. x) by AA, AS, P4, Def1; :: thesis: verum