theorem Th19: :: ANPROJ10:32

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