set M = 1. (K,n);
let M1 be Matrix of n,K; :: thesis: ex M being Matrix of n,K st
( M is invertible & M1 = ((M @) * M1) * M )
(((1. (K,n)) @) * M1) * (1. (K,n)) = ((1. (K,n)) * M1) * (1. (K,n)) by MATRIX_6:10
.= M1 * (1. (K,n)) by MATRIX_3:18
.= M1 by MATRIX_3:19 ;
hence ex M being Matrix of n,K st
( M is invertible & M1 = ((M @) * M1) * M ) ; :: thesis: verum