∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} [inst_2 : Field L] (φ : Polynomial K →+* L)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)) (x : K),
  (RatFunc.liftRingHom φ hφ) (RatFunc.C x) = φ (Polynomial.C x)