let n be Nat; :: thesis: for A, B, C, D, E being Matrix of n,REAL holds (A * ((B * C) * D)) * E = ((A * B) * C) * (D * E)
let A, B, C, D, E be Matrix of n,REAL; :: thesis: (A * ((B * C) * D)) * E = ((A * B) * C) * (D * E)
(A * ((B * C) * D)) * E = (A * (B * (C * D))) * E by MATRIXR2:28
.= A * ((B * (C * D)) * E) by MATRIXR2:28
.= A * (B * ((C * D) * E)) by MATRIXR2:28
.= A * (B * (C * (D * E))) by MATRIXR2:28
.= A * ((B * C) * (D * E)) by MATRIXR2:28
.= (A * (B * C)) * (D * E) by MATRIXR2:28
.= ((A * B) * C) * (D * E) by MATRIXR2:28 ;
hence (A * ((B * C) * D)) * E = ((A * B) * C) * (D * E) ; :: thesis: verum