theorem RFP: :: NEWTON04:8

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