(1_Rmatrix n) * (1_Rmatrix n) = 1_Rmatrix n by Th70;
hence 1_Rmatrix n is invertible by Def5; :: thesis: verum