let x, y, X, Y, Z be set ; :: thesis: 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))
let f be Function of [:X,Y:],Z; :: thesis: for g being Function st Z <> {} & x in X & y in Y holds
(g * f) . (x,y) = g . (f . (x,y))
let g be Function; :: thesis: ( Z <> {} & x in X & y in Y implies (g * f) . (x,y) = g . (f . (x,y)) )
assume A1: Z <> {} ; :: thesis: ( not x in X or not y in Y or (g * f) . (x,y) = g . (f . (x,y)) )
assume ( x in X & y in Y ) ; :: thesis: (g * f) . (x,y) = g . (f . (x,y))
then [x,y] in [:X,Y:] by ZFMISC_1:87;
hence (g * f) . (x,y) = g . (f . (x,y)) by A1, FUNCT_2:15; :: thesis: verum