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