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