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 Th13
.= (quotadd I) . v,u by Def12 ;
hence (quotadd I) . u,v = (quotadd I) . v,u ; :: thesis: verum