let n be Element of NAT ; :: thesis: Inv (1_Rmatrix n) = 1_Rmatrix n
( (1_Rmatrix n) * (1_Rmatrix n) = 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