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