:: deftheorem defines Z_Lin RLVECT_X:def 2 :
for V being RealLinearSpace
for A being Subset of V holds Z_Lin A = { (Sum l) where l is Linear_Combination of A : rng l c= INT } ;