∀ {ι : Type u_6} {A : Type u_1} {B : Type u_5} {C : Type u_3} {σ : Type u_2} {τ : Type u_7} {ψ : Type u_4}
  [inst : Semiring A] [inst_1 : Semiring B] [inst_2 : Semiring C] [inst_3 : SetLike σ A] [inst_4 : SetLike τ B]
  [inst_5 : SetLike ψ C] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ψ} (g : ℬ →+*ᵍ 𝒞) (f : 𝒜 →+*ᵍ ℬ) {i : ι} {x : A},
  x ∈ 𝒜 i → ((↑g).comp ↑f) x ∈ 𝒞 i