for i being natural Number
for p, q being FinSequence
for f being Permutation of (Seg i) st i <= len p & q = p * f holds
len q = i