theorem :: RELSET_3:33

for i1, i2 being Integer holds (addRel (INT,i1)) * (addRel (INT,i2)) = addRel (INT,(i1 + i2))