let Z be open Subset of REAL; :: thesis: for n being Element of NAT
for x being Real st x in Z holds
((diff (exp_R,Z)) . n) . x = exp_R . x
let n be Element of 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:70 ;
hence ((diff (exp_R,Z)) . n) . x = exp_R . x ; :: thesis: verum