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