(R : Type u) →
  [inst : Semiring R] →
    (ι : Type v) →
      (M : ι → Type w) →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] →
            [DecidableEq ι] → (s : Finset ι) → ((i : ↑↑s) → M ↑i) →ₗ[R] DirectSum ι fun i => M i