let m be non empty Element of NAT ; :: thesis: for f being PartFunc of (REAL m),REAL
for r being Real
for x being Element of REAL m st f is_differentiable_in x holds
( r (#) f is_differentiable_in x & diff ((r (#) f),x) = r (#) (diff (f,x)) )
let f be PartFunc of (REAL m),REAL; :: thesis: for r being Real
for x being Element of REAL m st f is_differentiable_in x holds
( r (#) f is_differentiable_in x & diff ((r (#) f),x) = r (#) (diff (f,x)) )
let r be Real; :: thesis: for x being Element of REAL m st f is_differentiable_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: ( f is_differentiable_in x implies ( r (#) f is_differentiable_in x & diff ((r (#) f),x) = r (#) (diff (f,x)) ) )
assume f is_differentiable_in x ; :: thesis: ( r (#) f is_differentiable_in x & diff ((r (#) f),x) = r (#) (diff (f,x)) )
then P1: <>* f is_differentiable_in x by PDIFF_7:def 1;
then P2: r (#) (<>* f) is_differentiable_in x by PDIFF_6:22;
r (#) (<>* f) = <>* (r (#) f) by LMXTh11;
hence r (#) f is_differentiable_in x by P2, PDIFF_7:def 1; :: thesis: diff ((r (#) f),x) = r (#) (diff (f,x))
thus diff ((r (#) f),x) = (proj (1,1)) * (diff ((r (#) (<>* f)),x)) by LMXTh11
.= (proj (1,1)) * (r (#) (diff ((<>* f),x))) by P1, PDIFF_6:22
.= r (#) (diff (f,x)) by INTEGR15:16 ; :: thesis: verum