∀ {Γ : Type u_1} {Γ' : Type u_4} {R : Type u_2} {V : Type u_5} {α : Type u_3} [inst : AddCommMonoid Γ]
  [inst_1 : PartialOrder Γ] [inst_2 : PartialOrder Γ'] [inst_3 : AddAction Γ Γ'] [inst_4 : IsOrderedCancelVAdd Γ Γ']
  [inst_5 : Semiring R] [inst_6 : AddCommMonoid V] [inst_7 : Module R V] (x : HahnSeries Γ R)
  (x_1 x_2 : HahnSeries.SummableFamily Γ' V α), x • (x_1 + x_2) = x • x_1 + x • x_2