let I be non degenerated commutative domRing-like Ring; 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; (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)))
; verum