let K be Field; :: thesis: for n being Nat
for M1, M2, M3, M4 being Matrix of n,K st M3 is_reverse_of M1 & M4 is_reverse_of M2 holds
M3 * M4 is_reverse_of M2 * M1
let n be Nat; :: thesis: for M1, M2, M3, M4 being Matrix of n,K st M3 is_reverse_of M1 & M4 is_reverse_of M2 holds
M3 * M4 is_reverse_of M2 * M1
let M1, M2, M3, M4 be Matrix of n,K; :: thesis: ( M3 is_reverse_of M1 & M4 is_reverse_of M2 implies M3 * M4 is_reverse_of M2 * M1 )
A1: ( width M1 = n & width M2 = n & width M3 = n & len M1 = n & len M2 = n & len M3 = n & width M4 = n & len M4 = n ) by MATRIX_1:25;
assume A2: ( M3 is_reverse_of M1 & M4 is_reverse_of M2 ) ; :: thesis: M3 * M4 is_reverse_of M2 * M1
A3: ( width (M3 * M4) = n & width (M2 * M1) = n ) by MATRIX_1:25;
then A4: (M3 * M4) * (M2 * M1) = ((M3 * M4) * M2) * M1 by A1, MATRIX_3:35
.= (M3 * (M4 * M2)) * M1 by A1, MATRIX_3:35
.= (M3 * (1. K,n)) * M1 by A2, Def2
.= M3 * M1 by MATRIX_3:21
.= 1. K,n by A2, Def2 ;
(M2 * M1) * (M3 * M4) = ((M2 * M1) * M3) * M4 by A1, A3, MATRIX_3:35
.= (M2 * (M1 * M3)) * M4 by A1, MATRIX_3:35
.= (M2 * (1. K,n)) * M4 by A2, Def2
.= M2 * M4 by MATRIX_3:21
.= 1. K,n by A2, Def2 ;
hence M3 * M4 is_reverse_of M2 * M1 by A4, Def2; :: thesis: verum