let I be non degenerated commutative domRing-like Ring; :: thesis: for u, v, w being Element of Quot. I holds
( qadd u,(qadd v,w) = qadd (qadd u,v),w & qadd u,v = qadd v,u )
let u, v, w be Element of Quot. I; :: thesis: ( qadd u,(qadd v,w) = qadd (qadd u,v),w & qadd u,v = qadd v,u )
consider x being Element of Q. I such that
A1: u = QClass. x by Def5;
consider y being Element of Q. I such that
A2: v = QClass. y by Def5;
A3: qadd u,v = QClass. (padd x,y) by A1, A2, Th11
.= qadd v,u by A1, A2, Th11 ;
consider z being Element of Q. I such that
A4: w = QClass. z by Def5;
qadd u,(qadd v,w) = qadd (QClass. x),(QClass. (padd y,z)) by A1, A2, A4, Th11
.= QClass. (padd x,(padd y,z)) by Th11
.= QClass. (padd (padd x,y),z) by Th4
.= qadd (QClass. (padd x,y)),(QClass. z) by Th11
.= qadd (qadd u,v),w by A1, A2, A4, Th11 ;
hence ( qadd u,(qadd v,w) = qadd (qadd u,v),w & qadd u,v = qadd v,u ) by A3; :: thesis: verum