theorem Th36: :: HFDIFF_1:36

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