theorem :: RELSET_3:68

for i being Integer holds multRel (INT,i) = { [i1,(i1 * i)] where i1 is Integer : verum }