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