A1: <i> = [*0 ,1,0 ,0 *] by Lm3, QUATERNI:def 6;
A2: (<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 A1, 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 * 1))*] by QUATERNI:def 10
.= - [*0 ,1,0 ,0 *] by QUATERN2:4 ;
thus <i> ^3 = - <i> by A2, Lm3, QUATERNI:def 6; :: thesis: verum