A2: ( <e2> . 1 = 0 & <e2> . 2 = 1 & <e2> . 3 = 0 ) by FINSEQ_1:62;
1 * <e2> = |[(1 * 0 ),(1 * 1),(1 * 0 )]| by A2, Lm3
.= <e2> ;
hence 1 * <e2> = <e2> ; :: thesis: verum