theorem Th1: :: POLYALG1:1

for X, Y being set
for f being Function of [:X,Y:],X holds dom f = [:X,Y:]