theorem Th42: :: FLEXARY1:42

for f being Function-yielding Function
for g being FinSequence
for x, y being object holds (g *. f) _ (x,y) = g . (f _ (x,y))