theorem Th21: :: BALLOT_1:8

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