(<k> * <k> ) * <k> = [*((((0 * 0 ) - (0 * 0 )) - (0 * 0 )) - (1 * 1)),((((0 * 0 ) + (0 * 0 )) + (0 * 1)) - (1 * 0 )),((((0 * 0 ) + (0 * 0 )) + (0 * 1)) - (1 * 0 )),((((0 * 1) + (1 * 0 )) + (0 * 0 )) - (0 * 0 ))*] * [*0 ,0 ,0 ,1*] by QUATERNI:def 10
.= [*(((((- 1) * 0 ) - (0 * 0 )) - (0 * 0 )) - (0 * 1)),(((((- 1) * 0 ) + (0 * 0 )) + (0 * 1)) - (0 * 0 )),(((((- 1) * 0 ) + (0 * 0 )) + (0 * 0 )) - (1 * 0 )),(((((- 1) * 1) + (0 * 0 )) + (0 * 0 )) - (0 * 0 ))*] by QUATERNI:def 10
.= - [*0 ,0 ,0 ,1*] by QUATERN2:4 ;
hence <k> ^3 = - <k> ; :: thesis: verum