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 Def10
.=
[*0 ,1,0 ,0 *]
;
<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 Def10
.=
[*0 ,(- 1),0 ,0 *]
;
then (<j> * <k> ) + (<k> * <j> ) =
[*(0 + 0 ),(0 + 0 ),(0 + 0 ),(1 + (- 1))*]
by A1, Def7
.=
0
by Lm7
;
hence
<j> * <k> = - (<k> * <j> )
by Def8; verum