theorem Th2: :: POLYALG1:2

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