theorem :: BINOP_1:18

for x, y being object
for X, Y, Z being set
for f being Function of [:X,Y:],Z
for g being Function st Z <> {} & x in X & y in Y holds
(g * f) . (x,y) = g . (f . (x,y)) by FUNCT_2:15, ZFMISC_1:87;