theorem Th17: :: MFOLD_2:17

for n being Nat
for X being set holds
( X is Linear_Combination of RealVectSpace (Seg n) iff X is Linear_Combination of TOP-REAL n )