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