theorem :: FUNCT_4:55

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