theorem Th7: :: REAL_NS2:7

for n being Nat
for p, q being Element of (TOP-REAL n)
for f, g being Element of (REAL-NS n) st p = f & q = g holds
p + q = f + g