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