let i, i1 be Integer; :: thesis: [i1,(i1 * i)] in multRel (INT,i)
( i1 in INT & i1 * i in INT ) by INT_1:def 2;
hence [i1,(i1 * i)] in multRel (INT,i) by Th42; :: thesis: verum