let n be Element of 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_1:25;
( width A = n & len B = n ) by MATRIX_1:25;
hence (A * B) * C = A * (B * C) by A1, MATRIX_3:35; :: thesis: verum