theorem :: RINGFRAC:47

for A being domRing holds the_Field_of_Quotients A is_ringisomorph_to Total-Quotient-Ring A