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