theorem :: MATGRP_0:64

for R being Ring
for n being Nat
for A, B, C being Matrix of n,R holds (A * B) * C = A * (B * C)