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