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 Th13
.= 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