{ι : Type u_1} →
  {A : ι → Type u_2} →
    [inst : Add ι] →
      [inst_1 : (i : ι) → AddCommMonoid (A i)] →
        {motive : DirectSum.GNonUnitalNonAssocSemiring A → Sort u} →
          (t : DirectSum.GNonUnitalNonAssocSemiring A) →
            ([toGMul : GradedMonoid.GMul A] →
                (mul_zero : ∀ {i j : ι} (a : A i), GradedMonoid.GMul.mul a 0 = 0) →
                  (zero_mul : ∀ {i j : ι} (b : A j), GradedMonoid.GMul.mul 0 b = 0) →
                    (mul_add :
                        ∀ {i j : ι} (a : A i) (b c : A j),
                          GradedMonoid.GMul.mul a (b + c) = GradedMonoid.GMul.mul a b + GradedMonoid.GMul.mul a c) →
                      (add_mul :
                          ∀ {i j : ι} (a b : A i) (c : A j),
                            GradedMonoid.GMul.mul (a + b) c = GradedMonoid.GMul.mul a c + GradedMonoid.GMul.mul b c) →
                        motive
                          { toGMul := toGMul, mul_zero := mul_zero, zero_mul := zero_mul, mul_add := mul_add,
                            add_mul := add_mul }) →
              motive t