for X being RealNormSpace
for x being sequence of X holds RAT_Sums (rng x) is countable Subset of the carrier of (ClNLin (rng x))