for n being Element of NAT
for x0 being Element of (REAL-US n)
for B being Subset of (REAL-US n) st B = RN_Base n holds
ex l being Linear_Combination of B st x0 = Sum l