let p be real number ; :: thesis: for f being PartFunc of REAL ,REAL st f = compreal holds
( (1 / 2) (#) (exp_R - (exp_R * f)) is_differentiable_in p & diff ((1 / 2) (#) (exp_R - (exp_R * f))),p = (1 / 2) * (diff (exp_R - (exp_R * f)),p) )
let f be PartFunc of REAL ,REAL ; :: thesis: ( f = compreal implies ( (1 / 2) (#) (exp_R - (exp_R * f)) is_differentiable_in p & diff ((1 / 2) (#) (exp_R - (exp_R * f))),p = (1 / 2) * (diff (exp_R - (exp_R * f)),p) ) )
assume f = compreal ; :: thesis: ( (1 / 2) (#) (exp_R - (exp_R * f)) is_differentiable_in p & diff ((1 / 2) (#) (exp_R - (exp_R * f))),p = (1 / 2) * (diff (exp_R - (exp_R * f)),p) )
then ( p is Real & exp_R - (exp_R * f) is_differentiable_in p ) by Lm15, XREAL_0:def 1;
hence ( (1 / 2) (#) (exp_R - (exp_R * f)) is_differentiable_in p & diff ((1 / 2) (#) (exp_R - (exp_R * f))),p = (1 / 2) * (diff (exp_R - (exp_R * f)),p) ) by FDIFF_1:23; :: thesis: verum