let M1 be Matrix of n,K; :: thesis: ex M being Matrix of n,K st
( M is invertible & M1 = ((M ~ ) * M1) * M )
take 1. K,n ; :: thesis: ( 1. K,n is invertible & M1 = (((1. K,n) ~ ) * M1) * (1. K,n) )
(((1. K,n) ~ ) * M1) * (1. K,n) = ((1. K,n) * M1) * (1. K,n) by MATRIX_6:8
.= M1 * (1. K,n) by MATRIX_3:20
.= M1 by MATRIX_3:21 ;
hence ( 1. K,n is invertible & M1 = (((1. K,n) ~ ) * M1) * (1. K,n) ) by MATRIX_6:8; :: thesis: verum