theorem :: FINSEQ_3:23

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