theorem :: MATRIXR2:79

for n being Nat holds Inv (1_Rmatrix n) = 1_Rmatrix n