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