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