theorem :: HFDIFF_1:51

for Z being open Subset of REAL st Z c= dom ln & Z c= dom ((id REAL) ^) holds
ln `| Z = ((id REAL) ^) | Z