:: deftheorem defines RAT_Sums NORMSP_4:def 1 :
for X being RealLinearSpace
for A being Subset of X holds RAT_Sums A = { (Sum l) where l is Linear_Combination of A : rng l c= RAT } ;