let R be Ring; :: thesis: for n being Nat
for A, B, C being Matrix of n,R holds (A * B) * C = A * (B * C)
let n be Nat; :: thesis: for A, B, C being Matrix of n,R holds (A * B) * C = A * (B * C)
let A, B, C be Matrix of n,R; :: thesis: (A * B) * C = A * (B * C)
( len A = n & width A = n & width B = n & len B = n & width C = n & len C = n ) by MATRIX_0:24;
hence (A * B) * C = A * (B * C) by MATRIX_3:33; :: thesis: verum