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