A1: <i> = [*0 ,1,0 ,0 *] by Def6', Lmx;
then A2: <k> * <i> = [*((((0 * 0 ) - (0 * 1)) - (0 * 0 )) - (1 * 0 )),((((0 * 1) + (0 * 0 )) + (0 * 0 )) - (1 * 0 )),((((0 * 0 ) + (0 * 0 )) + (1 * 1)) - (0 * 0 )),((((0 * 0 ) + (1 * 0 )) + (0 * 0 )) - (0 * 1))*] by Def10
.= [*0 ,0 ,1,0 *] ;
<i> * <k> = [*((((0 * 0 ) - (1 * 0 )) - (0 * 0 )) - (0 * 1)),((((0 * 0 ) + (1 * 0 )) + (0 * 1)) - (0 * 0 )),((((0 * 0 ) + (0 * 0 )) + (0 * 1)) - (1 * 1)),((((0 * 1) + (0 * 0 )) + (1 * 0 )) - (0 * 0 ))*] by A1, Def10
.= [*0 ,0 ,(- 1),0 *] ;
then (<k> * <i> ) + (<i> * <k> ) = [*(0 + 0 ),(0 + 0 ),(1 + (- 1)),(0 + 0 )*] by A2, Def7
.= 0 by Lm5 ;
hence <k> * <i> = - (<i> * <k> ) by Def8; :: thesis: verum