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