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

A2: now :: thesis: for x being object st x in dom (exp_R `| REAL) holds
(exp_R `| REAL) . x = (exp_R | REAL) . x

let x be object ; :: 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 ;
reconsider z1 = z as Element of REAL by XREAL_0:def 1;
(exp_R `| REAL) . x = diff (exp_R,z) by A3, FDIFF_1:def 7, TAYLOR_1:16;
then (exp_R `| REAL) . x = exp_R . z1 by TAYLOR_1:16;
hence (exp_R `| REAL) . x = (exp_R | REAL) . x ; :: thesis: verum

end;

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