theorem Th72: :: MATRIXR2:72

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