theorem Th30: :: HFDIFF_1:30

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