for K being Ring
for n being Nat
for p being Element of Permutations n
for i being Nat st i in Seg n holds
p . i in Seg n