let p be FinSequence of REAL ; :: thesis: for N1, M, N2 being Matrix of 3,REAL st len p = 3 holds
((N1 * M) * N2) * p = N1 * (M * (N2 * p))
let N1, M, N2 be Matrix of 3,REAL; :: thesis: ( len p = 3 implies ((N1 * M) * N2) * p = N1 * (M * (N2 * p)) )
assume A1: len p = 3 ; :: thesis: ((N1 * M) * N2) * p = N1 * (M * (N2 * p))
A2: ( width M = 3 & len M = 3 & width N1 = 3 & len N2 = 3 & width N2 = 3 ) by MATRIX_0:24;
A3: len (N2 * p) = 3 by A1, A2, MATRIXR1:61;
A4: ( len p = width N2 & width (N1 * M) = len N2 & len p > 0 & len N2 > 0 ) by MATRIXR2:4, A2, A1;
N1 * (M * (N2 * p)) = (N1 * M) * (N2 * p) by A3, A2, MATRIXR2:59
.= ((N1 * M) * N2) * p by A4, MATRIXR2:59 ;
hence ((N1 * M) * N2) * p = N1 * (M * (N2 * p)) ; :: thesis: verum