( <e3> . 1 = 0 & <e3> . 2 = 0 & <e3> . 3 = 1 ) by FINSEQ_1:45;
then 1 * <e3> = |[(1 * 0),(1 * 0),(1 * 1)]| by Lm1
.= <e3> ;
hence 1 * <e3> = <e3> ; :: thesis: verum