let p be real number ; :: 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:70, XREAL_0:def 1;
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:70 ;
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