let i be Integer; :: thesis: multRel (INT,i) = { [i1,(i1 * i)] where i1 is Integer : verum }
set S = { [i1,(i1 * i)] where i1 is Integer : verum } ;

now :: thesis: for o being object holds
( ( o in multRel (INT,i) implies o in { [i1,(i1 * i)] where i1 is Integer : verum } ) & ( o in { [i1,(i1 * i)] where i1 is Integer : verum } implies o in multRel (INT,i) ) )

let o be object ; :: thesis: ( ( o in multRel (INT,i) implies o in { [i1,(i1 * i)] where i1 is Integer : verum } ) & ( o in { [i1,(i1 * i)] where i1 is Integer : verum } implies o in multRel (INT,i) ) )

hereby :: thesis: ( o in { [i1,(i1 * i)] where i1 is Integer : verum } implies o in multRel (INT,i) )

assume A1: o in multRel (INT,i) ; :: thesis: o in { [i1,(i1 * i)] where i1 is Integer : verum }
then consider x, y being object such that
A2: o = [x,y] by RELAT_1:def 1;
reconsider x = x, y = y as set by TARSKI:1;
[x,y] in multRel (INT,i) by A1, A2;
then ( x in INT & y in INT ) by MMLQUER2:4;
then reconsider x = x, y = y as Integer ;
y = i * x by A1, A2, Th42;
hence o in { [i1,(i1 * i)] where i1 is Integer : verum } by A2; :: thesis: verum

end;

assume o in { [i1,(i1 * i)] where i1 is Integer : verum } ; :: thesis: o in multRel (INT,i)
then consider i1 being Integer such that
A3: o = [i1,(i1 * i)] ;
( i1 in INT & i1 * i in INT ) by INT_1:def 2;
hence o in multRel (INT,i) by A3, Th42; :: thesis: verum

end;

hence multRel (INT,i) = { [i1,(i1 * i)] where i1 is Integer : verum } by TARSKI:2; :: thesis: verum