theorem :: QUOFIELD:38

for I being non degenerated commutative domRing-like Ring holds
( 1. (the_Field_of_Quotients I) = q1. I & 0. (the_Field_of_Quotients I) = q0. I ) ;