for RS being RealLinearSpace
for f being FinSequence of RS st f = (Seg (len f)) --> (0. RS) holds
Sum f = 0. RS