let I be non degenerated commutative domRing-like Ring; for u, v, w being Element of Quot. I holds
( qmult (u,(qmult (v,w))) = qmult ((qmult (u,v)),w) & qmult (u,v) = qmult (v,u) )
let u, v, w be Element of Quot. I; ( qmult (u,(qmult (v,w))) = qmult ((qmult (u,v)),w) & qmult (u,v) = qmult (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: qmult (u,v) =
QClass. (pmult (x,y))
by A1, A3, Th10
.=
qmult (v,u)
by A1, A3, Th10
;
qmult (u,(qmult (v,w))) =
qmult ((QClass. x),(QClass. (pmult (y,z))))
by A1, A3, A2, Th10
.=
QClass. (pmult (x,(pmult (y,z))))
by Th10
.=
QClass. (pmult ((pmult (x,y)),z))
by Th4
.=
qmult ((QClass. (pmult (x,y))),(QClass. z))
by Th10
.=
qmult ((qmult (u,v)),w)
by A1, A3, A2, Th10
;
hence
( qmult (u,(qmult (v,w))) = qmult ((qmult (u,v)),w) & qmult (u,v) = qmult (v,u) )
by A4; verum