∀ (K : Type u_1) [inst : CommRing K] (toFractionRing toFractionRing_1 : FractionRing (Polynomial K)),
  ({ toFractionRing := toFractionRing } + { toFractionRing := toFractionRing_1 }).toFractionRing =
    { toFractionRing := toFractionRing }.toFractionRing + { toFractionRing := toFractionRing_1 }.toFractionRing