set IT = n -placesOf R;

reconsider f = {[{},{}]} as Function ;

ITT is Function-like ;

hence for b_{1} being Relation of (n -tuples_on X),(n -tuples_on Y) st b_{1} = n -placesOf R holds

b_{1} is Function-like
; :: thesis: verum

reconsider f = {[{},{}]} as Function ;

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

x in f

then reconsider ITT = n -placesOf R as Subset of f by TARSKI:def 3;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;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

ITT is Function-like ;

hence for b

b