∀ {α : Type u_1} {R : Type u_2} [inst : CommRing R] (F : Multiplicative (Multiset α) →* R),
  { toFun := fun s => (Multiset.map (fun x => F (Multiplicative.ofAdd {x})) (Multiplicative.toAdd s)).prod,
      map_one' := ⋯, map_mul' := ⋯ } =
    F