<e1> <X> <e2> = |[((0 * 0) - (0 * 1)),((0 * 0) - (1 * 0)),((1 * 1) - (0 * 0))]| by Lm15
.= <e3> ;
hence <e1> <X> <e2> = <e3> ; :: thesis: verum