theorem Th71: :: MATRIXR2:71

for n being Nat
for A being Matrix of n,REAL holds A * (1_Rmatrix n) = A