theorem Th9: :: EUCLID_3:9

for p1, p2 being Point of (TOP-REAL 2) holds euc2cpx (p1 + p2) = (euc2cpx p1) + (euc2cpx p2)