theorem :: HFDIFF_1:27

for x, r being Real
for n being Element of NAT
for Z being open Subset of REAL st x in Z holds
((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x)