thus multint is commutative :: thesis: multint is associative

proof

let i1 be Element of INT ; :: according to BINOP_1:def 13 :: thesis: for b₁ being Element of INT holds multint . i1,b₁ = multint . b₁,i1
let i2 be Element of INT ; :: thesis: multint . i1,i2 = multint . i2,i1
thus multint . i1,i2 = i1 * i2 by Def22
.= multint . i2,i1 by Def22 ; :: thesis: verum

end;

let i1 be Element of INT ; :: according to BINOP_1:def 14 :: thesis: for b₁, b₂ being Element of INT holds multint . i1,(multint . b₁,b₂) = multint . (multint . i1,b₁),b₂
let i2, i3 be Element of INT ; :: thesis: multint . i1,(multint . i2,i3) = multint . (multint . i1,i2),i3
thus multint . i1,(multint . i2,i3) = i1 * (multint . i2,i3) by Def22
.= i1 * (i2 * i3) by Def22
.= (i1 * i2) * i3
.= (multint . i1,i2) * i3 by Def22
.= multint . (multint . i1,i2),i3 by Def22 ; :: thesis: verum