for X being RealNormSpace
for w being Point of X
for e being Real
for l being Linear_Combination of {w} st 0 < e holds
ex m being Linear_Combination of {w} st
( Carrier m = Carrier l & rng m c= RAT & ||.((Sum l) - (Sum m)).|| < e )