theorem :: FINSEQ_2:55

for k being natural Number holds idseq k is Permutation of (Seg k) ;