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

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