∀ {ι : Type u_1} {F : Type u_2} {E : Type u_3} {x : ι → E} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  AlgHomClass (↥(IntermediateField.adjoin F (Set.range x)) ≃ₐ[F] FractionRing (MvPolynomial ι F)) F
    (↥(IntermediateField.adjoin F (Set.range x))) (FractionRing (MvPolynomial ι F))