let p be real number ; :: thesis: for f being PartFunc of REAL ,REAL st f = compreal holds
exp_R . ((- 1) * p) = (exp_R * f) . p
let f be PartFunc of REAL ,REAL ; :: thesis: ( f = compreal implies exp_R . ((- 1) * p) = (exp_R * f) . p )
assume A1: f = compreal ; :: thesis: exp_R . ((- 1) * p) = (exp_R * f) . p
A2: p is Real by XREAL_0:def 1;
exp_R . ((- 1) * p) = exp_R . (f . p) by A1, Lm11
.= (exp_R * f) . p by A1, A2, FUNCT_2:21 ;
hence exp_R . ((- 1) * p) = (exp_R * f) . p ; :: thesis: verum