∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : PartialOrder Γ']
  {f : Γ ↪o Γ'} {x : HahnSeries Γ R}, (HahnSeries.embDomain f x).support ⊆ ⇑f '' x.support