thus multrat is commutative :: thesis: multrat is associative

proof

let w1, w2 be Element of RAT ; :: according to BINOP_1:def 13 :: thesis: multrat . w1,w2 = multrat . w2,w1
thus multrat . w1,w2 = w1 * w2 by Def17
.= multrat . w2,w1 by Def17 ; :: thesis: verum

end;

let w1, w2, w3 be Element of RAT ; :: according to BINOP_1:def 14 :: thesis: multrat . w1,(multrat . w2,w3) = multrat . (multrat . w1,w2),w3
thus multrat . w1,(multrat . w2,w3) = w1 * (multrat . w2,w3) by Def17
.= w1 * (w2 * w3) by Def17
.= (w1 * w2) * w3
.= (multrat . w1,w2) * w3 by Def17
.= multrat . (multrat . w1,w2),w3 by Def17 ; :: thesis: verum