theorem Th30: :: MATRIX_3:30

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 I,D
for X being Element of Fin I
for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ (Y,((curry f) . i)) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ ([:X,Y:],f) = F $$ (X,g)