∀ {I : Type u_7} [inst : DecidableEq I] {R : I → Type u_8} [inst_1 : (i : I) → NonAssocSemiring (R i)] [Finite I]
  {S : Type u_9} [inst_3 : NonAssocSemiring S] {g h : ((i : I) → R i) →+* S},
  g = h ↔ ∀ (i : I) (x : R i), g (Pi.single i x) = h (Pi.single i x)