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