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