let n be Nat; :: thesis: for A being Matrix of n,REAL holds (1_Rmatrix n) * A = A
let A be Matrix of n,REAL; :: thesis: (1_Rmatrix n) * A = A
n = len A by MATRIX_0:def 2;
hence (1_Rmatrix n) * A = A by Th68; :: thesis: verum