let n be Element of NAT ; :: thesis: for A being Matrix of n, REAL holds A * (1_Rmatrix n) = A
let A be Matrix of n, REAL ; :: thesis: A * (1_Rmatrix n) = A
A1: n = len A by MATRIX_1:def 3;

now

per cases ( n <> 0 or n = 0 ) ;

case n <> 0 ; :: thesis: n = width A

then n > 0 ;
hence n = width A by A1, MATRIX_1:20; :: thesis: verum

end;

case n = 0 ; :: thesis: n = width A

hence n = width A by A1, MATRIX_1:def 4; :: thesis: verum

end;

end;

end;

hence A * (1_Rmatrix n) = A by Th67; :: thesis: verum