A1: len <e2> = 3 by CARD_1:def 7;
( <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 ) by EUCLID_8:def 2;
hence ( Col (<*<e2>*>,1) = <*0*> & Col (<*<e2>*>,2) = <*1*> & Col (<*<e2>*>,3) = <*0*> ) by A1, Th51; :: thesis: verum