theorem :: HFDIFF_1:40

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