thus multrat is commutative :: thesis: multrat is associative

proof

let w1, w2 be Element of RAT ; :: according to BINOP_1:def 2 :: 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 3 :: 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