theorem Th70: :: MATRIXR2:70

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