A1: <i> = [*0,1,0,0*] by Lm3, Lm4;
then A2: <k> * <i> = [*((((0 * 0) - (0 * 1)) - (0 * 0)) - (1 * 0)),((((0 * 1) + (0 * 0)) + (0 * 0)) - (1 * 0)),((((0 * 0) + (0 * 0)) + (1 * 1)) - (0 * 0)),((((0 * 0) + (1 * 0)) + (0 * 0)) - (0 * 1))*] by Def10
.= [*0,0,1,0*] ;
<i> * <k> = [*((((0 * 0) - (1 * 0)) - (0 * 0)) - (0 * 1)),((((0 * 0) + (1 * 0)) + (0 * 1)) - (0 * 0)),((((0 * 0) + (0 * 0)) + (0 * 1)) - (1 * 1)),((((0 * 1) + (0 * 0)) + (1 * 0)) - (0 * 0))*] by A1, Def10
.= [*0,0,(- 1),0*] ;
then (<k> * <i>) + (<i> * <k>) = [*(0 + 0),(0 + 0),(1 + (- 1)),(0 + 0)*] by A2, Def7
.= 0 by Lm7 ;
hence <k> * <i> = - (<i> * <k>) by Def8; :: thesis: verum