∀ {I : Type u_1} {f : I → Type u_3} {g : I → Type u_2} {r : (i : I) → Semiring (f i)}
  {m : (i : I) → AddCommMonoid (g i)} [inst : (i : I) → Module (f i) (g i)] (r_1 s : (i : I) → f i) (x : (i : I) → g i),
  (r_1 + s) • x = r_1 • x + s • x