for p being FinSequence
for x being object st x in dom p holds
x is Element of NAT ;