∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring A]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜]
  [inst_6 : (i : ι) → (x : ↥(𝒜 i)) → Decidable (x ≠ 0)] (r : A) (i : ι),
  i ∈ DFinsupp.support ((DirectSum.decompose 𝒜) r) ↔ (GradedRing.proj 𝒜 i) r ≠ 0