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