for n being Nat
for p being Point of (TOP-REAL n)
for V being Subset of (TOP-REAL n) st V = RN_Base n holds
ex l being Linear_Combination of V st p = Sum l