∀ {Γ : Type u_2} {Γ' : Type u_3} [inst : PartialOrder Γ] [inst_1 : PartialOrder Γ'] {R : Type u_4} [inst_2 : CommRing R]
  {U : Type u_5} {V : Type u_6} {W : Type u_1} [inst_3 : AddCommGroup U] [inst_4 : Module R U] [inst_5 : AddCommGroup V]
  [inst_6 : Module R V] [inst_7 : AddCommGroup W] [inst_8 : Module R W] (A : HVertexOperator Γ R V W)
  (B : HVertexOperator Γ' R U V) (x y : U),
  (HahnModule.of R) (A.compHahnSeries B (x + y)).ofIterate =
    (HahnModule.of R) (A.compHahnSeries B x).ofIterate + (HahnModule.of R) (A.compHahnSeries B y).ofIterate