(R : Type u) →
  [inst : Semiring R] →
    {ι : Type v} →
      {α : ι → Type u_1} →
        {δ : (i : ι) → α i → Type w} →
          [DecidableEq ι] →
            [inst_2 : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] →
              [inst_3 : (i : ι) → (j : α i) → Module R (δ i j)] →
                (DirectSum ((x : ι) × α x) fun i => δ i.fst i.snd) ≃ₗ[R]
                  DirectSum ι fun i => DirectSum (α i) fun j => δ i j