∀ {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (s : Subsemiring R)
  (f : R →+* S) (hf : Function.Injective ⇑f) (x x_1 : ↥s),
  (Equiv.Set.image (⇑f) (↑s) hf).toFun (x * x_1) =
    (Equiv.Set.image (⇑f) (↑s) hf).toFun x * (Equiv.Set.image (⇑f) (↑s) hf).toFun x_1