thus addrat is commutative :: thesis: addrat is associative

proof

let w1, w2 be Element of RAT ; :: according to BINOP_1:def 2 :: thesis: addrat . (w1,w2) = addrat . (w2,w1)
thus addrat . (w1,w2) = w1 + w2 by Def15
.= addrat . (w2,w1) by Def15 ; :: thesis: verum

end;

let w1, w2, w3 be Element of RAT ; :: according to BINOP_1:def 3 :: thesis: addrat . (w1,(addrat . (w2,w3))) = addrat . ((addrat . (w1,w2)),w3)
thus addrat . (w1,(addrat . (w2,w3))) = w1 + (addrat . (w2,w3)) by Def15
.= w1 + (w2 + w3) by Def15
.= (w1 + w2) + w3
.= (addrat . (w1,w2)) + w3 by Def15
.= addrat . ((addrat . (w1,w2)),w3) by Def15 ; :: thesis: verum