theorem Th75: :: MATGRP_0:63

for n being Nat
for L being non empty doubleLoopStr
for A, B being Matrix of n,L
for X, Y being Element of (Matrix_ring (n,L)) st A = X & B = Y holds
A * B = X * Y by Def5;