for p being Element of REAL 3 holds p = |[(p . 1),(p . 2),(p . 3)]|