set IT = n -placesOf R;
reconsider f = {[{},{}]} as Function ;

now :: thesis: for x being object st x in n -placesOf R holds
x in f

let x be object ; :: thesis: ( x in n -placesOf R implies x in f )
assume x in n -placesOf R ; :: thesis: x in f
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 ) ) ;
( p = {} & q = {} ) ;
hence x in f by TARSKI:def 1, A1; :: thesis: verum

end;

then reconsider ITT = n -placesOf R as Subset of f by TARSKI:def 3;
ITT is Function-like ;
hence for b₁ being Relation of (n -tuples_on X),(n -tuples_on Y) st b₁ = n -placesOf R holds
b₁ is Function-like ; :: thesis: verum