theorem Th5: :: HILB10_7:5

for y being object
for s being FinSequence st s " {y} <> {} holds
ex p being Permutation of (Seg (len s)) st
( (s * p) . (len s) = y & p = p " )