let f be FinSequence; :: thesis: idseq (len f) is Permutation of (dom f)
Seg (len f) = dom f by FINSEQ_1:def 3;
hence idseq (len f) is Permutation of (dom f) by FINSEQ_2:55; :: thesis: verum