∀ {R : Type u} {M : Type v} {ι : Type x} [inst : Semiring R] {φ : ι → Type i} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : DecidableEq ι]
  (f : (i : ι) → φ i →ₗ[R] M) (i j : ι) (x : φ i), (f j) (Pi.single i x j) = Pi.single i ((f i) x) j