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