let p be Element of REAL 3; :: thesis: p <X> |[0,0,0]| = |[0,0,0]|
p = |[(p . 1),(p . 2),(p . 3)]| by Th1;
hence p <X> |[0,0,0]| = |[(((p . 2) * 0) - ((p . 3) * 0)),(((p . 3) * 0) - ((p . 1) * 0)),(((p . 1) * 0) - ((p . 2) * 0))]| by Lm13
.= |[0,0,0]| ;
:: thesis: verum