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