let I be non degenerated commutative domRing-like Ring; :: thesis: 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; :: thesis: ( 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 y being Element of Q. I such that
A2: v = QClass. y by Def5;
A3: qmult u,v = QClass. (pmult x,y) by A1, A2, Th12
.= qmult v,u by A1, A2, Th12 ;
consider z being Element of Q. I such that
A4: w = QClass. z by Def5;
qmult u,(qmult v,w) = qmult (QClass. x),(QClass. (pmult y,z)) by A1, A2, A4, Th12
.= QClass. (pmult x,(pmult y,z)) by Th12
.= QClass. (pmult (pmult x,y),z) by Th5
.= qmult (QClass. (pmult x,y)),(QClass. z) by Th12
.= qmult (qmult u,v),w by A1, A2, A4, Th12 ;
hence ( qmult u,(qmult v,w) = qmult (qmult u,v),w & qmult u,v = qmult v,u ) by A3; :: thesis: verum