{ι : Type uι} →
  {R : Type uR} →
    {A : ι → Type uA} →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (A i)] →
          [inst_2 : (i : ι) → Module R (A i)] →
            [inst_3 : AddMonoid ι] →
              [inst_4 : DirectSum.GSemiring A] →
                {motive : DirectSum.GAlgebra R A → Sort u} →
                  ((toFun : R →+ A 0) →
                      (map_one : toFun 1 = GradedMonoid.GOne.one) →
                        (map_mul :
                            ∀ (r s : R),
                              GradedMonoid.mk 0 (toFun (r * s)) =
                                GradedMonoid.mk (0 + 0) (GradedMonoid.GMul.mul (toFun r) (toFun s))) →
                          (commutes :
                              ∀ (r : R) (x : GradedMonoid A),
                                GradedMonoid.mk 0 (toFun r) * x = x * GradedMonoid.mk 0 (toFun r)) →
                            (smul_def : ∀ (r : R) (x : GradedMonoid A), r • x = GradedMonoid.mk 0 (toFun r) * x) →
                              motive
                                { toFun := toFun, map_one := map_one, map_mul := map_mul, commutes := commutes,
                                  smul_def := smul_def }) →
                    (t : DirectSum.GAlgebra R A) → motive t