theorem :: RELSET_3:67

for i, i1 being Integer holds [i1,(i1 * i)] in multRel (INT,i)