A1: <j> * <j> =
[*((((0 * 0) - (0 * 0)) - (1 * 1)) - (0 * 0)),((((0 * 0) + (0 * 0)) + (0 * 0)) - (0 * 1)),((((0 * 1) + (0 * 1)) + (0 * 0)) - (0 * 0)),((((0 * 0) + (0 * 0)) + (0 * 1)) - (1 * 0))*]
by Def9
.=
[*(- 1),0,0,0*]
;
[*(- 1),0,0,0*] = [*(- jj),zz*]
by Lm3;
hence
<j> * <j> = - 1
by A1, ARYTM_0:def 5; verum