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