theorem Th23: :: MATRIX_3:23

for I, J, D being non empty set
for F, G being BinOp of D
for f being Function of I,D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st F is commutative & F is associative & ( [:Y,X:] <> {} or F is having_a_unity ) & G is commutative holds
F $$ ([:X,Y:],(G * (f,g))) = F $$ ([:Y,X:],(G * (g,f)))