<i> = [*0,1,0,0*] by Lm3, Lm4;
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, Lm4; :: thesis: verum