for RS being RealLinearSpace
for f being FinSequence of RS
for x, y being Element of RS
for a, b being Integer st x in Z_Lin f & y in Z_Lin f holds
(a * x) + (b * y) in Z_Lin f