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