( <e1> . 1 = 1 & <e1> . 2 = 0 & <e1> . 3 = 0 ) by FINSEQ_1:62;
then |(<e1> ,<e1> )| = ((1 * 1) + (0 * 0 )) + (0 * 0 ) by Lm8
.= 1 ;
hence |(<e1> ,<e1> )| = 1 ; :: thesis: verum