thus addint is commutative :: thesis: addint is associative

proof

let i1, i2 be Element of INT ; :: according to BINOP_1:def 13 :: 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 14 :: 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