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 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; :: thesis: verum