for n being Nat
for X being Subspace of RealVectSpace (Seg n)
for x, y being Element of REAL n st x in the carrier of X & y in the carrier of X holds
x + y in the carrier of X