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