:: deftheorem defines has_Field_of_Quotients_Pair QUOFIELD:def 26 :
for I, F being non empty doubleLoopStr
for f being Function of I,F holds
( I has_Field_of_Quotients_Pair F,f iff ( f is RingMonomorphism & ( for F9 being non empty non degenerated right_complementable almost_left_invertible Abelian add-associative right_zeroed associative commutative well-unital distributive doubleLoopStr
for f9 being Function of I,F9 st f9 is RingMonomorphism holds
ex h being Function of F,F9 st
( h is RingHomomorphism & h * f = f9 & ( for h9 being Function of F,F9 st h9 is RingHomomorphism & h9 * f = f9 holds
h9 = h ) ) ) ) );