theorem Th57: :: FUNCT_4:57

for X, X9, Y, Y9 being set
for f, g being Function st dom f c= [:X,Y:] & dom g c= [:X9,Y9:] holds
dom |:f,g:| c= [:[:X,X9:],[:Y,Y9:]:]