:: deftheorem defines 0_Rmatrix MATRIXR1:def 8 :
for n, m being Nat holds 0_Rmatrix (n,m) = MXF2MXR (0. (F_Real,n,m));