theorem :: QUOFIELD:31

for I being non degenerated commutative domRing-like Ring
for u, v being Element of (the_Field_of_Quotients I) holds (quotadd I) . (u,v) is Element of (the_Field_of_Quotients I)