for n, m being Nat
for A being Matrix of REAL holds
( ( n = width A implies A * (1_Rmatrix n) = A ) & ( m = len A implies (1_Rmatrix m) * A = A ) ) by Th67, Th68;