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