let f be FinSequence; :: thesis: Rev (idseq (len f)) is Permutation of (dom (Rev f))
dom (Rev f) = dom f by FINSEQ_5:57
.= Seg (len f) by FINSEQ_1:def 3 ;
hence Rev (idseq (len f)) is Permutation of (dom (Rev f)) by MATRIX94; :: thesis: verum