theorem Th99: :: FUNCT_4:99
for f being Function
for x, y being object holds dom (f +~ (x,y)) = dom f