let I be non degenerated commutative domRing-like Ring; 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; ( 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; verum