thus multint is commutative :: thesis: multint is associative

proof

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