theorem :: HFDIFF_1:39

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