A1: dom (exp_R | REAL ) = REAL /\ REAL by RELAT_1:90, TAYLOR_1:16;

A2: now

let x be set ; :: thesis: ( x in dom (exp_R `| REAL ) implies (exp_R `| REAL ) . x = (exp_R | REAL ) . x )
assume A3: x in dom (exp_R `| REAL ) ; :: thesis: (exp_R `| REAL ) . x = (exp_R | REAL ) . x
then reconsider z = x as real number ;
reconsider z1 = z as Real by XREAL_0:def 1;
(exp_R `| REAL ) . x = diff exp_R ,z by A3, FDIFF_1:def 8, TAYLOR_1:16;
then (exp_R `| REAL ) . x = exp_R . z1 by TAYLOR_1:16;
hence (exp_R `| REAL ) . x = (exp_R | REAL ) . x by A1, FUNCT_1:70; :: thesis: verum

end;

dom (exp_R `| REAL ) = REAL by FDIFF_1:def 8, TAYLOR_1:16;
then exp_R `| REAL = exp_R | REAL by A1, A2, FUNCT_1:9;
hence exp_R is_integral_of exp_R , REAL by Lm1, TAYLOR_1:16; :: thesis: verum