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