let n be Element of NAT ; for K being Field
for A, B, C being Matrix of n,K holds (A * B) * C = A * (B * C)
let K be Field; for A, B, C being Matrix of n,K holds (A * B) * C = A * (B * C)
let A, B, C be Matrix of n,K; (A * B) * C = A * (B * C)
A1:
( width B = n & len C = n )
by MATRIX_0:24;
( width A = n & len B = n )
by MATRIX_0:24;
hence
(A * B) * C = A * (B * C)
by A1, MATRIX_3:33; verum