thus addrat is commutative :: thesis: addrat is associative

proof

let w1 be Element of RAT ; :: according to BINOP_1:def 13 :: thesis: for b₁ being Element of RAT holds addrat . w1,b₁ = addrat . b₁,w1
let w2 be Element of RAT ; :: 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 be Element of RAT ; :: according to BINOP_1:def 14 :: thesis: for b₁, b₂ being Element of RAT holds addrat . w1,(addrat . b₁,b₂) = addrat . (addrat . w1,b₁),b₂
let w2, w3 be Element of RAT ; :: 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