theorem Th17: :: MATRIX14:17
for n being Element of NAT
for K being Field
for A, B, C being Matrix of n,K holds (A * B) * C = A * (B * C)