thus addint is commutative :: thesis: addint is associative

proof

let i1, i2 be Element of INT ; :: according to BINOP_1:def 2 :: thesis: addint . (i1,i2) = addint . (i2,i1)
thus addint . (i1,i2) = i1 + i2 by Def20
.= addint . (i2,i1) by Def20 ; :: thesis: verum

end;

let i1, i2, i3 be Element of INT ; :: according to BINOP_1:def 3 :: thesis: addint . (i1,(addint . (i2,i3))) = addint . ((addint . (i1,i2)),i3)
thus addint . (i1,(addint . (i2,i3))) = i1 + (addint . (i2,i3)) by Def20
.= i1 + (i2 + i3) by Def20
.= (i1 + i2) + i3
.= (addint . (i1,i2)) + i3 by Def20
.= addint . ((addint . (i1,i2)),i3) by Def20 ; :: thesis: verum