for p being FinSequence
for x being object
for k being Nat st k in dom p & k < x .. p holds
p . k <> x