theorem Th134: :: HILB10_7:134

for k being Nat
for y being object
for s being FinSequence st card (s " {y}) = k holds
ex p being Permutation of (dom s) ex s1 being FinSequence st
( s * p = s1 ^ (k |-> y) & not y in rng s1 )