let n be Nat; 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; (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)
; verum