<i> = [*0 ,1,0 ,0 *] by Def6', Lmx;
then A1: <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))*] by Def10
.= [*(- 1),0 ,0 ,0 *] ;
- 1 = [*(- 1),0 *] by ARYTM_0:def 7;
hence <i> * <i> = - 1 by A1, Def6'; :: thesis: verum