theorem Th1: :: HFDIFF_1:1

for Z being open Subset of REAL
for f being Function of REAL,REAL holds dom (f | Z) = Z