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