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