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