let M1 be Matrix of n,K; :: thesis: ex M being Matrix of n,K st
( M is invertible & M1 = ((M ~ ) * M1) * M )
A1: (((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 ;
take 1. K,n ; :: thesis: ( 1. K,n is invertible & M1 = (((1. K,n) ~ ) * M1) * (1. K,n) )
thus ( 1. K,n is invertible & M1 = (((1. K,n) ~ ) * M1) * (1. K,n) ) by A1, MATRIX_6:8; :: thesis: verum