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