let n be Nat; :: thesis: Inv (1_Rmatrix n) = 1_Rmatrix n
(1_Rmatrix n) * (1_Rmatrix n) = 1_Rmatrix n by Th70;
hence Inv (1_Rmatrix n) = 1_Rmatrix n by Def6; :: thesis: verum