theorem Th74: :: MATRIXJ1:74

for K being Field
for G, G9, G1, G2 being FinSequence_of_Matrix of K st len G = len G9 holds
(G ^ G1) (#) (G9 ^ G2) = (G (#) G9) ^ (G1 (#) G2)