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