for i, k being Nat
for p being FinSequence of REAL st p has_onlyone_value_in k & i <> k holds
p . i = 0