∀ {ιA : Type u_2} {ιB : Type u_3} (A : ιA → Type u_4) (M : ιB → Type u_1) [inst : AddMonoid ιA] [inst_1 : VAdd ιA ιB]
  [inst_2 : (i : ιA) → AddCommMonoid (A i)] [inst_3 : (i : ιB) → AddCommMonoid (M i)] [inst_4 : GradedMonoid.GMonoid A]
  [inst_5 : DirectSum.Gmodule A M] {i : ιA} {j : ιB} (a : A i) (b c : M j),
  GradedMonoid.GSMul.smul a (b + c) = GradedMonoid.GSMul.smul a b + GradedMonoid.GSMul.smul a c