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