theorem Th16: :: REAL_NS3:15

for n being Nat
for a being Real
for x, y being Element of (REAL-NS n)
for x0, y0 being Element of (RealVectSpace (Seg n)) st x = x0 & y = y0 holds
( the carrier of (REAL-NS n) = the carrier of (RealVectSpace (Seg n)) & 0. (REAL-NS n) = 0. (RealVectSpace (Seg n)) & x + y = x0 + y0 & a * x = a * x0 & - x = - x0 & x - y = x0 - y0 )