theorem Th64: :: MATRIXR2:64

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