theorem Th13: :: REAL_NS1:13

for n being Nat
for a being Real
for x1, y1 being Point of (REAL-NS n)
for x2, y2 being Point of (REAL-US n) st x1 = x2 & y1 = y2 holds
( x1 + y1 = x2 + y2 & - x1 = - x2 & a * x1 = a * x2 )