let p be Real; :: 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 )
A1: p in REAL by XREAL_0:def 1;
assume A2: f = compreal ; :: thesis: exp_R . ((- 1) * p) = (exp_R * f) . p
then exp_R . ((- 1) * p) = exp_R . (f . p) by Lm10
.= (exp_R * f) . p by A2, A1, FUNCT_2:15 ;
hence exp_R . ((- 1) * p) = (exp_R * f) . p ; :: thesis: verum