theorem Th54: :: FUNCT_4:54

for x, x9, y, y9 being object
for f, g being Function holds
( [[x,x9],[y,y9]] in dom |:f,g:| iff ( [x,y] in dom f & [x9,y9] in dom g ) )