∀ {ι : Type u_1} [inst : DecidableEq ι] (A : ι → Type u_2) [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] {i : ι} (a : A 0) (b : A i),
  (DirectSum.of A i) (a • b) = (DirectSum.of A 0) a * (DirectSum.of A i) b