∀ {R : Type u_5} {ι₁ : Type u_1} {ι₂ : Type u_2} [inst : CommSemiring R] {N₁ : Type u_3} [inst_1 : AddCommMonoid N₁]
  [inst_2 : Module R N₁] {N₂ : Type u_4} [inst_3 : AddCommMonoid N₂] [inst_4 : Module R N₂] {N : ι₁ ⊕ ι₂ → Type u_6}
  [inst_5 : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)] [inst_6 : (i : ι₁ ⊕ ι₂) → Module R (N i)]
  (a : MultilinearMap R (fun i₁ => N (Sum.inl i₁)) N₁) (b : MultilinearMap R (fun i₂ => N (Sum.inr i₂)) N₂)
  [inst_7 : DecidableEq (ι₁ ⊕ ι₂)] (m : (i : ι₁ ⊕ ι₂) → N i) (i : ι₁ ⊕ ι₂) (c : R) (x : N i),
  ((a fun i₁ => Function.update m i (c • x) (Sum.inl i₁)) ⊗ₜ[R] b fun i₂ => Function.update m i (c • x) (Sum.inr i₂)) =
    c • (a fun i₁ => Function.update m i x (Sum.inl i₁)) ⊗ₜ[R] b fun i₂ => Function.update m i x (Sum.inr i₂)