theorem :: NEWTON04:7

for f being FinSequence holds idseq (len f) is Permutation of (dom f)