for I being commutative domRing-like Ring
for F, F9 being non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for f being Function of I,F
for f9 being Function of I,F9 st I has_Field_of_Quotients_Pair F,f & I has_Field_of_Quotients_Pair F9,f9 holds
F is_ringisomorph_to F9