theorem Th2: :: PARTFUN3:2

for f being non-empty real-valued Function holds dom (f ^) = dom f