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