theorem Th19: :: FUNCT_1:19

for X being set
for f being Function holds dom (f * (id X)) = (dom f) /\ X