∀ {X Y S : AlgebraicGeometry.Scheme} [inst : X.Over S] [inst_1 : Y.Over S] {f : X.RationalMap Y},
  AlgebraicGeometry.Scheme.RationalMap.IsOver S f ↔
    f.compHom (Y ↘ S) = AlgebraicGeometry.Scheme.Hom.toRationalMap (X ↘ S)