let Z be open Subset of REAL; :: thesis: for n being Nat

for x being Real st x in Z holds

((diff (exp_R,Z)) . n) . x = exp_R . x

let n be Nat; :: thesis: for x being Real st x in Z holds

((diff (exp_R,Z)) . n) . x = exp_R . x

let x be Real; :: thesis: ( x in Z implies ((diff (exp_R,Z)) . n) . x = exp_R . x )

assume x in Z ; :: thesis: ((diff (exp_R,Z)) . n) . x = exp_R . x

then A1: x in dom (exp_R | Z) by Th5;

((diff (exp_R,Z)) . n) . x = (exp_R | Z) . x by Th6

.= exp_R . x by A1, FUNCT_1:47 ;

hence ((diff (exp_R,Z)) . n) . x = exp_R . x ; :: thesis: verum

for x being Real st x in Z holds

((diff (exp_R,Z)) . n) . x = exp_R . x

let n be Nat; :: thesis: for x being Real st x in Z holds

((diff (exp_R,Z)) . n) . x = exp_R . x

let x be Real; :: thesis: ( x in Z implies ((diff (exp_R,Z)) . n) . x = exp_R . x )

assume x in Z ; :: thesis: ((diff (exp_R,Z)) . n) . x = exp_R . x

then A1: x in dom (exp_R | Z) by Th5;

((diff (exp_R,Z)) . n) . x = (exp_R | Z) . x by Th6

.= exp_R . x by A1, FUNCT_1:47 ;

hence ((diff (exp_R,Z)) . n) . x = exp_R . x ; :: thesis: verum