let x0 be real number ; :: thesis: for f being PartFunc of REAL ,REAL st f is_differentiable_in x0 holds
( exp_R * f is_differentiable_in x0 & diff (exp_R * f),x0 = (exp_R . (f . x0)) * (diff f,x0) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( f is_differentiable_in x0 implies ( exp_R * f is_differentiable_in x0 & diff (exp_R * f),x0 = (exp_R . (f . x0)) * (diff f,x0) ) )
A1: x0 is Real by XREAL_0:def 1;
assume A2: f is_differentiable_in x0 ; :: thesis: ( exp_R * f is_differentiable_in x0 & diff (exp_R * f),x0 = (exp_R . (f . x0)) * (diff f,x0) )
A3: exp_R is_differentiable_in f . x0 by Th16, FDIFF_1:16;
hence exp_R * f is_differentiable_in x0 by A1, A2, FDIFF_2:13; :: thesis: diff (exp_R * f),x0 = (exp_R . (f . x0)) * (diff f,x0)
thus diff (exp_R * f),x0 = (diff exp_R ,(f . x0)) * (diff f,x0) by A1, A2, A3, FDIFF_2:13
.= (exp_R . (f . x0)) * (diff f,x0) by Th16 ; :: thesis: verum