let x0 be Real; :: 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)) ) )

assume A1: 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)) )

A2: ( x0 is Real & exp_R is_differentiable_in f . x0 ) by Th16, FDIFF_1:9, XREAL_0:def 1;

hence exp_R * f is_differentiable_in x0 by A1, 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, FDIFF_2:13

.= (exp_R . (f . x0)) * (diff (f,x0)) by Th16 ; :: thesis: verum

( 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)) ) )

assume A1: 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)) )

A2: ( x0 is Real & exp_R is_differentiable_in f . x0 ) by Th16, FDIFF_1:9, XREAL_0:def 1;

hence exp_R * f is_differentiable_in x0 by A1, 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, FDIFF_2:13

.= (exp_R . (f . x0)) * (diff (f,x0)) by Th16 ; :: thesis: verum