theorem :: ANPROJ_8:61

( (1_Rmatrix 3) . 1 = <e1> & (1_Rmatrix 3) . 2 = <e2> & (1_Rmatrix 3) . 3 = <e3> ) by MATRIXR2:77, MATRIXR2:78, EUCLID_8:def 1, EUCLID_8:def 2, EUCLID_8:def 3;