theorem :: QUOFIELD:34

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