theorem Th32: :: MATRIX_3:32

for D, I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ ([:X,Y:],f) = F $$ (Y,g)