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