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