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