theorem Th30: :: MATRIX14:30

for n being Element of NAT
for K being Field
for A, B being Matrix of n,K holds (A * B) @ = (B @) * (A @)