for n being Nat
for p, q1, q2 being Point of (TOP-REAL n) holds |(p,(q1 + q2))| = |(p,q1)| + |(p,q2)| by Th16;