( len <e1> = 3 & <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 ) by EUCLID_8:def 1, FINSEQ_1:45;
hence <*<e1>*> @ = F2M <e1> by DEF1, Th57; :: thesis: ( <*<e2>*> @ = F2M <e2> & <*<e3>*> @ = F2M <e3> )
( len <e2> = 3 & <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 ) by EUCLID_8:def 2, FINSEQ_1:45;
hence <*<e2>*> @ = F2M <e2> by DEF1, Th57; :: thesis: <*<e3>*> @ = F2M <e3>
( len <e3> = 3 & <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 ) by EUCLID_8:def 3, FINSEQ_1:45;
hence <*<e3>*> @ = F2M <e3> by DEF1, Th57; :: thesis: verum