theorem :: ANPROJ10:24

for x, y being Element of (TOP-REAL 1)
for p, q being Tuple of 1, REAL st p = x & q = y holds
x + y = p + q ;