∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} {M₅ : Type u_1} {M₆ : Type u_2}
  [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : AddCommMonoid M₄] [inst_5 : AddCommMonoid M₅] [inst_6 : AddCommMonoid M₆] [inst_7 : Module R M]
  [inst_8 : Module R M₂] [inst_9 : Module R M₃] [inst_10 : Module R M₄] [inst_11 : Module R M₅] [inst_12 : Module R M₆]
  (f₁₂ : M →ₗ[R] M₂) (f₂₃ : M₂ →ₗ[R] M₃) (g₁₂ : M₄ →ₗ[R] M₅) (g₂₃ : M₅ →ₗ[R] M₆),
  f₂₃.prodMap g₂₃ ∘ₗ f₁₂.prodMap g₁₂ = (f₂₃ ∘ₗ f₁₂).prodMap (g₂₃ ∘ₗ g₁₂)