theorem Th13: :: ENTROPY1:13

for k being Nat
for p being FinSequence of REAL st p has_onlyone_value_in k holds
Sum p = p . k