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