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