theorem Th17: :: NORMSP_4:13

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