theorem Th119: :: HILB10_7:119

for n being Nat
for F being finite set
for E being Enumeration of F
for p being Permutation of (dom E)
for S being Subset of (doms (n,(card F))) holds { (s * p) where s is FinSequence of NAT : s in S } is Subset of (doms (n,(card F)))