let j1, j2 be Integer; :: thesis: addint . j1,j2 = j1 + j2
reconsider i1 = j1, i2 = j2 as Element of INT by INT_1:def 2;
addint . i1,i2 = j1 + j2 by BINOP_2:def 20;
hence addint . j1,j2 = j1 + j2 ; :: thesis: verum