theorem Th31: :: RLVECT_X:31

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