for RS being RealLinearSpace
for f being FinSequence of RS
for i being Nat st i in Seg (len f) holds
f /. i in Z_Lin f