{I : Type u} →
  {f : I → Type v} →
    {γ : Type w} →
      [inst : (i : I) → NonUnitalNonAssocSemiring (f i)] →
        [inst_1 : NonUnitalNonAssocSemiring γ] → ((i : I) → γ →ₙ+* f i) → γ →ₙ+* (i : I) → f i