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