let n be Element of 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_1:def 2;
hence (1_Rmatrix n) * A = A by Th68; :: thesis: verum