:: deftheorem defines 1_Rmatrix MATRIXR2:def 2 :
for n being Nat holds 1_Rmatrix n = MXF2MXR (1. (F_Real,n));