(<j> * <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))*] * [*0,0,jj,0*]
by QUATERNI:def 10
.=
[*(((((- 1) * 0) - (0 * 0)) - (0 * 1)) - (0 * 0)),(((((- 1) * 0) + (0 * 0)) + (0 * 0)) - (0 * 1)),(((((- 1) * 1) + (0 * 0)) + (0 * 0)) - (0 * 0)),(((((- 1) * 0) + (0 * 0)) + (0 * 1)) - (0 * 0))*]
by QUATERNI:def 10
.=
- [*0,0,jj,0*]
by QUATERN2:4
;
hence
<j> ^3 = - <j>
; verum