:: deftheorem defines 0_Rmatrix MATRIXR2:def 3 :
for n being Nat holds 0_Rmatrix n = 0_Rmatrix (n,n);