let RS be RealLinearSpace; :: thesis: for f being FinSequence of RS holds rng f c= Z_Lin f
let f be FinSequence of RS; :: thesis: rng f c= Z_Lin f
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in Z_Lin f )
assume y in rng f ; :: thesis: y in Z_Lin f
then consider x being set such that
P1: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
P2: x in Seg (len f) by FINSEQ_1:def 3, P1;
reconsider i = x as Nat by P1;
y = f /. i by P1, PARTFUN1:def 8;
hence y in Z_Lin f by P2, SLM0200; :: thesis: verum