theorem :: QUOFIELD:30

for I being non degenerated commutative domRing-like Ring holds
( the carrier of (the_Field_of_Quotients I) = Quot. I & the addF of (the_Field_of_Quotients I) = quotadd I & the multF of (the_Field_of_Quotients I) = quotmult I & 0. (the_Field_of_Quotients I) = q0. I & 1. (the_Field_of_Quotients I) = q1. I ) ;