theorem :: EUCLID_8:34

for p being Element of REAL 3 holds 0 * p = |[0,0,0]|