∀ {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : FunLike F (Polynomial R) (Polynomial S)] [inst_3 : RingHomClass F (Polynomial R) (Polynomial S)] (φ : F)
  (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))) (x y : RatFunc R),
  (↑(RatFunc.map φ hφ)).toFun (x + y) = (↑(RatFunc.map φ hφ)).toFun x + (↑(RatFunc.map φ hφ)).toFun y