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