let n be Nat; :: thesis: for R being commutative Ring
for M1, M3 being Matrix of n,R st M3 is_reverse_of M1 & n > 0 holds
M1 @ is_reverse_of M3 @
let R be commutative Ring; :: thesis: for M1, M3 being Matrix of n,R st M3 is_reverse_of M1 & n > 0 holds
M1 @ is_reverse_of M3 @
let M1, M3 be Matrix of n,R; :: thesis: ( M3 is_reverse_of M1 & n > 0 implies M1 @ is_reverse_of M3 @ )
A1: ( width M1 = n & width M3 = n ) by MATRIX_0:24;
assume that
A2: M3 is_reverse_of M1 and
A3: n > 0 ; :: thesis: M1 @ is_reverse_of M3 @
( len M1 = n & M3 * M1 = M1 * M3 ) by A2, MATRIX_0:24;
then A4: (M1 * M3) @ = (M1 @) * (M3 @) by A1, A3, MATRIX_3:22;
then A5: (M1 @) * (M3 @) = 1. (R,n) by Th11, A2;
len M3 = n by MATRIX_0:24;
then (M3 @) * (M1 @) = (M1 @) * (M3 @) by A1, A3, A4, MATRIX_3:22;
hence M1 @ is_reverse_of M3 @ by A5; :: thesis: verum