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