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