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_1:25;
A5: len M = n by MATRIX_1:25;
A6: ( len M2 = n & width (M ~ ) = n ) by MATRIX_1:25;
A7: width M = n by MATRIX_1:25;
A8: ( len ((M ~ ) * M2) = n & width ((M ~ ) * M2) = n ) by MATRIX_1:25;
A9: len (M ~ ) = n by MATRIX_1:25;
(((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:35
.= (((M * (M ~ )) * M2) * M) * (M ~ ) by A7, A9, A6, MATRIX_3:35
.= (((1. K,n) * M2) * M) * (M ~ ) by A3, MATRIX_6:def 2
.= (M2 * M) * (M ~ ) by MATRIX_3:20
.= M2 * (M * (M ~ )) by A4, A5, A7, A9, MATRIX_3:35
.= M2 * (1. K,n) by A3, MATRIX_6:def 2
.= M2 by MATRIX_3:21 ;
hence ( M ~ is invertible & M2 = (((M ~ ) ~ ) * M1) * (M ~ ) ) by A1, MATRIX_6:16; :: thesis: verum