<i> = [*0,1,0,0*] by Lm2, Lm3;
then <i> * <j> = [*((((0 * 0) - (1 * 0)) - (0 * 1)) - (0 * 0)),((((0 * 0) + (1 * 0)) + (0 * 0)) - (0 * 1)),((((0 * 1) + (0 * 0)) + (0 * 0)) - (0 * 1)),((((0 * 0) + (0 * 0)) + (1 * 1)) - (0 * 0))*] by Def9
.= [*0,0,0,1*] ;
hence <i> * <j> = <k> ; :: thesis: verum