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) )
A1: p is Real by XREAL_0:def 1;
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 exp_R - (exp_R * f) is_differentiable_in p by Lm16;
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 A1, FDIFF_1:23; :: thesis: verum