for r being Real
for f being real-valued FinSequence st rng f c= {0,r} holds
Sum f = r * (card (f " {r}))