theorem Th65: :: FUNCT_3:65

for f, g being Function
for x, y being object st [x,y] in [:(dom f),(dom g):] holds
[:f,g:] . (x,y) = [(f . x),(g . y)]