theorem :: MATRIXR2:85
( 1_Rmatrix 0 = 0_Rmatrix 0 & 1_Rmatrix 0 = {} )