theorem :: MATRIXR2:85

( 1_Rmatrix 0 = 0_Rmatrix 0 & 1_Rmatrix 0 = {} )