theorem Th39: :: REAL_NS2:39

for n being Nat
for p being Element of (TOP-REAL n)
for f being Element of (REAL-NS n)
for H being Subset of (TOP-REAL n)
for I being Subset of (REAL-NS n) st p = f & H = I holds
p + H = f + I