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