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