theorem :: HFDIFF_1:44

for x0 being Real
for n being Element of NAT
for Z being open Subset of REAL st not 0 in Z & x0 in Z holds
(((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0))