∀ {R : Type u_1} {ι : Type u_2} {M' : Type u_3} {κ : ι → Type u_4} {M : (i : ι) → κ i → Type u_5}
  [inst : CommSemiring R] [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)]
  [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] [Finite ι]
  [inst_6 : (i : ι) → DecidableEq (κ i)] ⦃f g : MultilinearMap R (fun i => DirectSum (κ i) fun j => M i j) M'⦄,
  (∀ (p : (i : ι) → κ i),
      (f.compLinearMap fun i => DirectSum.lof R (κ i) (M i) (p i)) =
        g.compLinearMap fun i => DirectSum.lof R (κ i) (M i) (p i)) →
    f = g