theorem :: HFDIFF_1:31

for n being Element of NAT
for Z being open Subset of REAL st n >= 2 holds
(diff ((#Z n),Z)) . 3 = (((n * (n - 1)) * (n - 2)) (#) (#Z (n - 3))) | Z