theorem Th2: :: REAL_NS1:2

for n being Nat
for x, y being VECTOR of (REAL-NS n)
for a, b being Element of REAL n st x = a & y = b holds
x + y = a + b