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