theorem Th41: :: FINSEQ_2:43

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