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 z being Element of Q. I such that
A2: w = QClass. z by Def5;
consider y being Element of Q. I such that
A3: v = QClass. y by Def5;
A4: qadd (u,v) = QClass. (padd (x,y)) by A1, A3, Th9
.= qadd (v,u) by A1, A3, Th9 ;
qadd (u,(qadd (v,w))) = qadd ((QClass. x),(QClass. (padd (y,z)))) by A1, A3, A2, Th9
.= QClass. (padd (x,(padd (y,z)))) by Th9
.= QClass. (padd ((padd (x,y)),z)) by Th3
.= qadd ((QClass. (padd (x,y))),(QClass. z)) by Th9
.= qadd ((qadd (u,v)),w) by A1, A3, A2, Th9 ;
hence ( qadd (u,(qadd (v,w))) = qadd ((qadd (u,v)),w) & qadd (u,v) = qadd (v,u) ) by A4; :: thesis: verum