theorem Th30: :: MATRIXR2:30

for n being Nat
for A, B being Matrix of n,REAL holds (A * B) @ = (B @) * (A @)