theorem :: HFDIFF_1:52

for x0 being Real
for n being Element of NAT
for Z being open Subset of REAL st n >= 1 & x0 in Z & not 0 in Z holds
((diff (((#Z n) ^),Z)) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^) . x0)