for RS being RealLinearSpace
for f being FinSequence of RS
for v being Element of RS
for i being Nat st i in Seg (len f) & f = ((Seg (len f)) --> (0. RS)) +* ({i} --> v) holds
Sum f = v