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