thus
addrat is commutative
addrat is associative
let w1, w2, w3 be Element of RAT ; BINOP_1:def 3 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
; verum