let n be 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_0:def 2;

now :: thesis: ( ( n <> 0 & n = width A ) or ( n = 0 & n = width A ) )

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

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

hence n = width A by A1, MATRIX_0:20; :: thesis: verum

end;

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

hence n = width A by A1, MATRIX_0:def 3; :: thesis: verum

end;

end;

end;

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