theorem Th124: :: HILB10_7:124

for m being Nat
for F being finite set
for E being Enumeration of F
for p being Permutation of (dom E)
for s being FinSequence st s in doms (m,(card F)) holds
s * p in doms (m,(card F))