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 ) ;
end;
end;
hence A * (1_Rmatrix n) = A by Th67; :: thesis: verum