for p, q being Element of REAL 3 holds p + q = |[((p . 1) + (q . 1)),((p . 2) + (q . 2)),((p . 3) + (q . 3))]| by Lm2;