for n being Nat
for p1, p2 being Point of (TOP-REAL n)
for r1, r2 being real-valued Function st p1 = r1 & p2 = r2 holds
p1 + p2 = r1 + r2 ;