let Z be open Subset of REAL ; :: thesis: ( exp_R `| Z = exp_R | Z & dom (exp_R | Z) = Z )
A1: exp_R is_differentiable_on Z by FDIFF_1:34, TAYLOR_1:16;
then A2: dom (exp_R `| Z) = Z by FDIFF_1:def 8;
A3: dom (exp_R | Z) = Z by LemX;
for x being Real st x in Z holds
(exp_R `| Z) . x = (exp_R | Z) . x

proof

let x be Real; :: thesis: ( x in Z implies (exp_R `| Z) . x = (exp_R | Z) . x )
assume A4: x in Z ; :: thesis: (exp_R `| Z) . x = (exp_R | Z) . x
thus (exp_R `| Z) . x = diff exp_R ,x by A1, A4, FDIFF_1:def 8
.= exp_R . x by TAYLOR_1:16
.= (exp_R | Z) . x by A3, A4, FUNCT_1:70 ; :: thesis: verum

end;

hence ( exp_R `| Z = exp_R | Z & dom (exp_R | Z) = Z ) by A2, A3, PARTFUN1:34; :: thesis: verum