theorem :: EUCLID_7:37

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