for p being Element of REAL 3 holds |(p,(0.REAL 3))| = 0