theorem Th58: :: FUNCT_4:58

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