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:106;
hence (g * f) . x,y = g . (f . x,y) by A1, FUNCT_2:21; :: thesis: verum