len M = n by MATRIX_0:24;
then A1: len |:M:| = n by Def7;
width M = n by MATRIX_0:24;
then width |:M:| = n by Def7;
hence |:M:| is Matrix of n,REAL by A1, MATRIX_0:51; :: thesis: verum