for M being Matrix of REAL holds M + (0_Rmatrix ((len M),(width M))) = M