theorem Th51: :: FUNCT_2:52

for X being set
for f being Function of X,X holds dom f = X