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