let n be Nat; :: thesis: for R being Ring
for M1, M2, M3 being Matrix of n,R st M2 is_reverse_of M3 & M1 is_reverse_of M3 holds
M1 = M2
let R be Ring; :: thesis: for M1, M2, M3 being Matrix of n,R st M2 is_reverse_of M3 & M1 is_reverse_of M3 holds
M1 = M2
let M1, M2, M3 be Matrix of n,R; :: thesis: ( M2 is_reverse_of M3 & M1 is_reverse_of M3 implies M1 = M2 )
A1: ( width M1 = n & width M3 = n ) by MATRIX_0:24;
A2: ( len M2 = n & len M3 = n ) by MATRIX_0:24;
assume that
A3: M2 is_reverse_of M3 and
A4: M1 is_reverse_of M3 ; :: thesis: M1 = M2
M1 = M1 * (1. (R,n)) by MATRIX_3:19
.= M1 * (M3 * M2) by A3
.= (M1 * M3) * M2 by A1, A2, MATRIX_3:33
.= (1. (R,n)) * M2 by A4
.= M2 by MATRIX_3:18 ;
hence M1 = M2 ; :: thesis: verum