theorem :: HFDIFF_1:46

for Z being open Subset of REAL st not 0 in Z holds
((id REAL) ^) `| Z = ((- 1) (#) ((#Z 2) ^)) | Z