let I be non degenerated commutative domRing-like Ring; :: thesis: for u being Element of (the_Field_of_Quotients I) holds (quotmultinv I) . u is Element of (the_Field_of_Quotients I)
let u be Element of (the_Field_of_Quotients I); :: thesis: (quotmultinv I) . u is Element of (the_Field_of_Quotients I)
reconsider s = u as Element of Quot. I ;
(quotmultinv I) . u = qmultinv s by Def15;
hence (quotmultinv I) . u is Element of (the_Field_of_Quotients I) ; :: thesis: verum