A1: <j> * <j> = [*((((0 * 0 ) - (0 * 0 )) - (1 * 1)) - (0 * 0 )),((((0 * 0 ) + (0 * 0 )) + (0 * 0 )) - (0 * 1)),((((0 * 1) + (0 * 1)) + (0 * 0 )) - (0 * 0 )),((((0 * 0 ) + (0 * 0 )) + (0 * 1)) - (1 * 0 ))*] by Def10
.= [*(- 1),0 ,0 ,0 *] ;
[*(- 1),0 ,0 ,0 *] = [*(- 1),0 *] by Def6';
hence <j> * <j> = - 1 by A1, ARYTM_0:def 7; :: thesis: verum