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 object ; :: 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 object such that
A1: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
A2: x in Seg (len f) by A1, FINSEQ_1:def 3;
reconsider i = x as Nat by A1;
y = f /. i by A1, PARTFUN1:def 6;
hence y in Z_Lin f by A2, Th30; :: thesis: verum