set Xn = n -tuples_on X;
set Yn = n -tuples_on Y;
set IT = { [p,q] where p is Element of n -tuples_on X, q is Element of n -tuples_on Y : for j being set st j in Seg n holds
[(p . j),(q . j)] in R } ;

now :: thesis: for x being object st x in { [p,q] where p is Element of n -tuples_on X, q is Element of n -tuples_on Y : for j being set st j in Seg n holds
[(p . j),(q . j)] in R } holds
x in [:(n -tuples_on X),(n -tuples_on Y):]

let x be object ; :: thesis: ( x in { [p,q] where p is Element of n -tuples_on X, q is Element of n -tuples_on Y : for j being set st j in Seg n holds
[(p . j),(q . j)] in R } implies x in [:(n -tuples_on X),(n -tuples_on Y):] )
assume x in { [p,q] where p is Element of n -tuples_on X, q is Element of n -tuples_on Y : for j being set st j in Seg n holds
[(p . j),(q . j)] in R } ; :: thesis: x in [:(n -tuples_on X),(n -tuples_on Y):]
then consider p being Element of n -tuples_on X, q being Element of n -tuples_on Y such that
A1: ( x = [p,q] & ( for j being set st j in Seg n holds
[(p . j),(q . j)] in R ) ) ;
thus x in [:(n -tuples_on X),(n -tuples_on Y):] by A1; :: thesis: verum

end;

hence { [p,q] where p is Element of n -tuples_on X, q is Element of n -tuples_on Y : for j being set st j in Seg n holds
[(p . j),(q . j)] in R } is Relation of (n -tuples_on X),(n -tuples_on Y) by TARSKI:def 3; :: thesis: verum