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

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

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

dom (exp_R `| Z) = Z
by A1, FDIFF_1:def 7;
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;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

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