<i> = [*0,1,0,0*]
by Lm2, Lm3;
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 Def9
.=
[*0,0,1,0*]
;
hence
<k> * <i> = <j>
; verum