let M1, M2 be Matrix of n,K; :: thesis: ( ex M being Matrix of n,K st

( M is invertible & M1 = ((M ~) * M2) * M ) implies ex M being Matrix of n,K st

( M is invertible & M2 = ((M ~) * M1) * M ) )

given M being Matrix of n,K such that A1: M is invertible and

A2: M1 = ((M ~) * M2) * M ; :: thesis: ex M being Matrix of n,K st

( M is invertible & M2 = ((M ~) * M1) * M )

A3: M ~ is_reverse_of M by A1, MATRIX_6:def 4;

take M ~ ; :: thesis: ( M ~ is invertible & M2 = (((M ~) ~) * M1) * (M ~) )

A4: width M2 = n by MATRIX_0:24;

A5: len M = n by MATRIX_0:24;

A6: ( len M2 = n & width (M ~) = n ) by MATRIX_0:24;

A7: width M = n by MATRIX_0:24;

A8: ( len ((M ~) * M2) = n & width ((M ~) * M2) = n ) by MATRIX_0:24;

A9: len (M ~) = n by MATRIX_0:24;

(((M ~) ~) * M1) * (M ~) = (M * (((M ~) * M2) * M)) * (M ~) by A1, A2, MATRIX_6:16

.= ((M * ((M ~) * M2)) * M) * (M ~) by A5, A7, A8, MATRIX_3:33

.= (((M * (M ~)) * M2) * M) * (M ~) by A7, A9, A6, MATRIX_3:33

.= (((1. (K,n)) * M2) * M) * (M ~) by A3, MATRIX_6:def 2

.= (M2 * M) * (M ~) by MATRIX_3:18

.= M2 * (M * (M ~)) by A4, A5, A7, A9, MATRIX_3:33

.= M2 * (1. (K,n)) by A3, MATRIX_6:def 2

.= M2 by MATRIX_3:19 ;

hence ( M ~ is invertible & M2 = (((M ~) ~) * M1) * (M ~) ) by A1; :: thesis: verum

( M is invertible & M1 = ((M ~) * M2) * M ) implies ex M being Matrix of n,K st

( M is invertible & M2 = ((M ~) * M1) * M ) )

given M being Matrix of n,K such that A1: M is invertible and

A2: M1 = ((M ~) * M2) * M ; :: thesis: ex M being Matrix of n,K st

( M is invertible & M2 = ((M ~) * M1) * M )

A3: M ~ is_reverse_of M by A1, MATRIX_6:def 4;

take M ~ ; :: thesis: ( M ~ is invertible & M2 = (((M ~) ~) * M1) * (M ~) )

A4: width M2 = n by MATRIX_0:24;

A5: len M = n by MATRIX_0:24;

A6: ( len M2 = n & width (M ~) = n ) by MATRIX_0:24;

A7: width M = n by MATRIX_0:24;

A8: ( len ((M ~) * M2) = n & width ((M ~) * M2) = n ) by MATRIX_0:24;

A9: len (M ~) = n by MATRIX_0:24;

(((M ~) ~) * M1) * (M ~) = (M * (((M ~) * M2) * M)) * (M ~) by A1, A2, MATRIX_6:16

.= ((M * ((M ~) * M2)) * M) * (M ~) by A5, A7, A8, MATRIX_3:33

.= (((M * (M ~)) * M2) * M) * (M ~) by A7, A9, A6, MATRIX_3:33

.= (((1. (K,n)) * M2) * M) * (M ~) by A3, MATRIX_6:def 2

.= (M2 * M) * (M ~) by MATRIX_3:18

.= M2 * (M * (M ~)) by A4, A5, A7, A9, MATRIX_3:33

.= M2 * (1. (K,n)) by A3, MATRIX_6:def 2

.= M2 by MATRIX_3:19 ;

hence ( M ~ is invertible & M2 = (((M ~) ~) * M1) * (M ~) ) by A1; :: thesis: verum