∀ (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 ι] (i j : ι) (b : M j),
  (DirectSum.component R ι M i) ((DirectSum.lof R ι M j) b) = if h : j = i then Eq.recOn h b else 0