theorem :: ANPROJ_8:62

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