∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (i : ι) (m : M i),
  (DirectSum.linearEquivFunOnFintype R ι M).symm (Pi.single i m) = (DirectSum.lof R ι M i) m