let m be non zero 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 A1: <>* f is_differentiable_in x ;
then r (#) (<>* f) is_differentiable_in x by PDIFF_6:22;
hence r (#) f is_differentiable_in x by Th8; :: thesis: diff ((r (#) f),x) = r (#) (diff (f,x))
thus diff ((r (#) f),x) = (proj (1,1)) * (diff ((r (#) (<>* f)),x)) by Th8
.= (proj (1,1)) * (r (#) (diff ((<>* f),x))) by A1, PDIFF_6:22
.= r (#) (diff (f,x)) by INTEGR15:16 ; :: thesis: verum