A1: <j> * <k> = [*((((0 * 0) - (0 * 0)) - (1 * 0)) - (0 * 1)),((((0 * 0) + (0 * 0)) + (1 * 1)) - (0 * 0)),((((0 * 0) + (0 * 1)) + (0 * 0)) - (1 * 0)),((((0 * 1) + (0 * 0)) + (0 * 0)) - (1 * 0))*] by Def9
.= [*zz,jj,zz,zz*] ;
<k> * <j> = [*((((0 * 0) - (0 * 0)) - (0 * 1)) - (1 * 0)),((((0 * 0) + (0 * 0)) + (0 * 0)) - (1 * 1)),((((0 * 1) + (0 * 0)) + (0 * 1)) - (0 * 0)),((((0 * 0) + (1 * 0)) + (0 * 1)) - (0 * 0))*] by Def9
.= [*zz,(- jj),zz,zz*] ;
then (<j> * <k>) + (<k> * <j>) = [*(0 + 0),(0 + 0),(0 + 0),(1 + (- 1))*] by A1, Def6
.= 0 by Lm6 ;
hence <j> * <k> = - (<k> * <j>) by Def7; :: thesis: verum