let I be non degenerated commutative domRing-like Ring; :: thesis: I is_embedded_in the_Field_of_Quotients I
canHom I is embedding by Th57;
hence I is_embedded_in the_Field_of_Quotients I ; :: thesis: verum