theorem Th63: :: POLYNOM9:63

for n being Nat
for f being FinSequence of Seg n
for i being Nat st i in n & count_reps (f,n) = (EmptyBag n) +* (i,(len f)) holds
f = (len f) |-> (i + 1)