for n being Nat
for f being Permutation of (Seg n) holds f is FinSequence of Seg n