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 A1: x in Z ; :: thesis: ((diff exp_R ,Z) . n) . x = exp_R . x
A2: x in dom (exp_R | Z) by A1, Th5;
((diff exp_R ,Z) . n) . x = (exp_R | Z) . x by Th6
.= exp_R . x by A2, FUNCT_1:70 ;
hence ((diff exp_R ,Z) . n) . x = exp_R . x ; :: thesis: verum