theorem :: ANPROJ10:23

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