let p be Real; :: thesis: for f being PartFunc of REAL,REAL st f = compreal holds
( exp_R * f is_differentiable_in p & diff ((exp_R * f),p) = (- 1) * (exp_R . (f . p)) )
let f be PartFunc of REAL,REAL; :: thesis: ( f = compreal implies ( exp_R * f is_differentiable_in p & diff ((exp_R * f),p) = (- 1) * (exp_R . (f . p)) ) )
assume A1: f = compreal ; :: thesis: ( exp_R * f is_differentiable_in p & diff ((exp_R * f),p) = (- 1) * (exp_R . (f . p)) )
A2: ( p is Real & exp_R is_differentiable_in f . p ) by SIN_COS:65;
A3: f is_differentiable_in p by A1, Lm12;
then diff ((exp_R * f),p) = (diff (exp_R,(f . p))) * (diff (f,p)) by A2, FDIFF_2:13
.= (diff (exp_R,(f . p))) * (- 1) by A1, Lm12
.= (exp_R . (f . p)) * (- 1) by SIN_COS:65 ;
hence ( exp_R * f is_differentiable_in p & diff ((exp_R * f),p) = (- 1) * (exp_R . (f . p)) ) by A2, A3, FDIFF_2:13; :: thesis: verum