theorem Th54: :: POLYNOM9:54

for n being Nat holds count_reps ({},n) = EmptyBag n