for x1, x2, y1, y2 being Real holds |[x1,y1]| + |[x2,y2]| = |[(x1 + x2),(y1 + y2)]|