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