:: deftheorem defines the_Field_of_Quotients QUOFIELD:def 16 :
for I being non degenerated commutative domRing-like Ring holds the_Field_of_Quotients I = doubleLoopStr(# (Quot. I),(quotadd I),(quotmult I),(q1. I),(q0. I) #);