for RS being RealLinearSpace
for f being FinSequence of RS holds rng f c= Z_Lin f