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:18
.= M1 by MATRIX_3:19 ;
hence ( 1. (K,n) is invertible & M1 = (((1. (K,n)) ~) * M1) * (1. (K,n)) ) ; :: thesis: verum