theorem Th31: :: MATRIX_3:31

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 st F is having_a_unity & F is commutative & F is associative holds
for y being Element of J st ( for j being Element of J holds g . j = F $$ (X,((curry' f) . j)) ) holds
F $$ ([:X,{.y.}:],f) = F $$ ({.y.},g)