let n be Nat; :: thesis: for K being Field

for M1, M2, M3 being Matrix of n,K st M2 is_reverse_of M3 & M1 is_reverse_of M3 holds

M1 = M2

let K be Field; :: thesis: for M1, M2, M3 being Matrix of n,K st M2 is_reverse_of M3 & M1 is_reverse_of M3 holds

M1 = M2

let M1, M2, M3 be Matrix of n,K; :: 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. (K,n)) by MATRIX_3:19

.= M1 * (M3 * M2) by A3

.= (M1 * M3) * M2 by A1, A2, MATRIX_3:33

.= (1. (K,n)) * M2 by A4

.= M2 by MATRIX_3:18 ;

hence M1 = M2 ; :: thesis: verum

for M1, M2, M3 being Matrix of n,K st M2 is_reverse_of M3 & M1 is_reverse_of M3 holds

M1 = M2

let K be Field; :: thesis: for M1, M2, M3 being Matrix of n,K st M2 is_reverse_of M3 & M1 is_reverse_of M3 holds

M1 = M2

let M1, M2, M3 be Matrix of n,K; :: 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. (K,n)) by MATRIX_3:19

.= M1 * (M3 * M2) by A3

.= (M1 * M3) * M2 by A1, A2, MATRIX_3:33

.= (1. (K,n)) * M2 by A4

.= M2 by MATRIX_3:18 ;

hence M1 = M2 ; :: thesis: verum