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