theorem Th64: :: POLYNOM9:64

for i, n, m being Nat st i in n holds
count_reps ((m |-> (i + 1)),n) = (EmptyBag n) +* (i,m)