let p be FinSequence of REAL ; 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; ( len p = 3 implies ((N1 * M) * N2) * p = N1 * (M * (N2 * p)) )
assume A1:
len p = 3
; ((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))
; verum