A1:
<i> = [*zz,jj,zz,zz*]
by Lm2, Lm3;
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 Def9
.=
[*zz,zz,jj,zz*]
;
<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, Def9
.=
[*zz,zz,(- jj),zz*]
;
then (<k> * <i>) + (<i> * <k>) =
[*(0 + 0),(0 + 0),(1 + (- 1)),(0 + 0)*]
by A2, Def6
.=
0
by Lm6
;
hence
<k> * <i> = - (<i> * <k>)
by Def7; verum