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:26, TAYLOR_1:16;
A2: dom (exp_R | Z) = Z by Lm1;
A3: for x being Element of REAL st x in Z holds
(exp_R `| Z) . x = (exp_R | Z) . x
proof
let x be Element of 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 7
.= exp_R . x by TAYLOR_1:16
.= (exp_R | Z) . x by A2, A4, FUNCT_1:47 ; :: thesis: verum
end;
dom (exp_R `| Z) = Z by A1, FDIFF_1:def 7;
hence ( exp_R `| Z = exp_R | Z & dom (exp_R | Z) = Z ) by A2, A3, PARTFUN1:5; :: thesis: verum