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