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 r being Real st X c= dom f & f is_differentiable_on X holds
( r (#) f is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((r (#) f) `| X) /. x = r (#) ((f `| X) /. x) ) )
let X be Subset of (REAL m); :: thesis: for f being PartFunc of (REAL m),REAL
for r being Real st X c= dom f & f is_differentiable_on X holds
( r (#) f is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((r (#) f) `| X) /. x = r (#) ((f `| X) /. x) ) )
let f be PartFunc of (REAL m),REAL; :: thesis: for r being Real st X c= dom f & f is_differentiable_on X holds
( r (#) f is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((r (#) f) `| X) /. x = r (#) ((f `| X) /. x) ) )
let r be Real; :: thesis: ( X c= dom f & f is_differentiable_on X implies ( r (#) f is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((r (#) f) `| X) /. x = r (#) ((f `| X) /. x) ) ) )
assume AK: X c= dom f ; :: thesis: ( not f is_differentiable_on X or ( r (#) f is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((r (#) f) `| X) /. x = r (#) ((f `| X) /. x) ) ) )
assume AS1: f is_differentiable_on X ; :: thesis: ( r (#) f is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((r (#) f) `| X) /. x = r (#) ((f `| X) /. x) ) )
then P0: X is open by AK, YTh33;
P3: X c= dom (r (#) f) by AK, VALUED_1:def 5;

P5: now :: thesis: for x being Element of REAL m st x in X holds
( r (#) f is_differentiable_in x & diff ((r (#) f),x) = r (#) (diff (f,x)) )

let x be Element of REAL m; :: thesis: ( x in X implies ( r (#) f is_differentiable_in x & diff ((r (#) f),x) = r (#) (diff (f,x)) ) )
assume x in X ; :: thesis: ( r (#) f is_differentiable_in x & diff ((r (#) f),x) = r (#) (diff (f,x)) )
then f is_differentiable_in x by AS1, P0, AK, YTh32;
hence ( r (#) f is_differentiable_in x & diff ((r (#) f),x) = r (#) (diff (f,x)) ) by PDIFF622X; :: thesis: verum

end;

then for x being Element of REAL m st x in X holds
r (#) f is_differentiable_in x ;
hence r (#) f is_differentiable_on X by P3, P0, YTh32; :: thesis: for x being Element of REAL m st x in X holds
((r (#) f) `| X) /. x = r (#) ((f `| X) /. x)
let x be Element of REAL m; :: thesis: ( x in X implies ((r (#) f) `| X) /. x = r (#) ((f `| X) /. x) )
assume P7: x in X ; :: thesis: ((r (#) f) `| X) /. x = r (#) ((f `| X) /. x)
then ((r (#) f) `| X) /. x = diff ((r (#) f),x) by P3, XDef1;
hence ((r (#) f) `| X) /. x = r (#) (diff (f,x)) by P7, P5
.= r (#) ((f `| X) /. x) by AK, P7, XDef1 ;
:: thesis: verum