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