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

for M1, M3 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 M1, M3 being Matrix of n,K st M3 is_reverse_of M1 & n > 0 holds

M1 @ is_reverse_of M3 @

let M1, M3 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_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. (K,n) by Th10, 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

for M1, M3 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 M1, M3 being Matrix of n,K st M3 is_reverse_of M1 & n > 0 holds

M1 @ is_reverse_of M3 @

let M1, M3 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_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. (K,n) by Th10, 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