let K be Ring; :: 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 by MATRIX_0:24;
A2: ( width M2 = n & len M1 = n ) by MATRIX_0:24;
A3: len M3 = n by MATRIX_0:24;
A4: ( width M3 = n & len M4 = n ) by MATRIX_0:24;
assume that
A5: M3 is_reverse_of M1 and
A6: M4 is_reverse_of M2 ; :: thesis: M3 * M4 is_reverse_of M2 * M1
width (M2 * M1) = n by MATRIX_0:24;
then A7: (M2 * M1) * (M3 * M4) = ((M2 * M1) * M3) * M4 by A3, A4, MATRIX_3:33
.= (M2 * (M1 * M3)) * M4 by A1, A2, A3, MATRIX_3:33
.= (M2 * (1. (K,n))) * M4 by A5
.= M2 * M4 by MATRIX_3:19
.= 1. (K,n) by A6 ;
A8: width M4 = n by MATRIX_0:24;
A9: len M2 = n by MATRIX_0:24;
width (M3 * M4) = n by MATRIX_0:24;
then (M3 * M4) * (M2 * M1) = ((M3 * M4) * M2) * M1 by A2, A9, MATRIX_3:33
.= (M3 * (M4 * M2)) * M1 by A9, A8, A4, MATRIX_3:33
.= (M3 * (1. (K,n))) * M1 by A6
.= M3 * M1 by MATRIX_3:19
.= 1. (K,n) by A5 ;
hence M3 * M4 is_reverse_of M2 * M1 by A7; :: thesis: verum