let n be Nat; :: thesis: for K being Field
for M3, M1 being Matrix of n,K st M3 is_reverse_of M1 & n > 0 holds
M1 @ is_reverse_of M3 @
let K be Field; :: thesis: for M3, M1 being Matrix of n,K st M3 is_reverse_of M1 & n > 0 holds
M1 @ is_reverse_of M3 @
let M3, M1 be Matrix of n,K; :: thesis: ( M3 is_reverse_of M1 & n > 0 implies M1 @ is_reverse_of M3 @ )
A1: ( width M1 = n & width M3 = n ) by MATRIX_1: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, Def2, MATRIX_1:24;
then A4: (M1 * M3) @ = (M1 @) * (M3 @) by A1, A3, MATRIX_3:22;
M1 * M3 = 1. (K,n) by A2, Def2;
then A5: (M1 @) * (M3 @) = 1. (K,n) by A4, Th10;
len M3 = n by MATRIX_1:24;
then (M3 @) * (M1 @) = (M1 @) * (M3 @) by A1, A3, A4, MATRIX_3:22;
hence M1 @ is_reverse_of M3 @ by A5, Def2; :: thesis: verum