let n be Nat; :: thesis: for A, B, C being Matrix of n,REAL holds (A * B) * C = A * (B * C)
let A, B, C be Matrix of n,REAL; :: thesis: (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; :: thesis: verum