let I be non degenerated commutative domRing-like Ring; :: thesis: for u, v being Element of holds (quotmult I) . u,v is Element of
let u, v be Element of ; :: thesis: (quotmult I) . u,v is Element of
reconsider s = u as Element of Quot. I ;
reconsider t = v as Element of Quot. I ;
(quotmult I) . u,v = qmult s,t by Def13;
hence (quotmult I) . u,v is Element of ; :: thesis: verum