theorem Th77: :: FINSEQOP:77

for x, y being set
for F, f, g being Function st [x,y] in dom (F * (f,g)) holds
(F * (f,g)) . (x,y) = F . ((f . x),(g . y))