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