theorem :: RLVECT_X:33

for RS being RealLinearSpace
for f being non empty FinSequence of RS holds Z_Lin (rng f) = Z_Lin f