set RR = n -placesOf R;
set XX = n -tuples_on X;
A1: dom R = X by PARTFUN1:def 2;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;

now :: thesis: for x being object st x in n -tuples_on X holds
x in dom (n -placesOf R)

let x be object ; :: thesis: ( x in n -tuples_on X implies x in dom (n -placesOf R) )
assume x in n -tuples_on X ; :: thesis: x in dom (n -placesOf R)
then reconsider xx = x as Element of n -tuples_on X ;
reconsider xxx = xx as Element of Funcs ((Seg n),X) by FOMODEL0:11;
defpred S₁[ set , set ] means [(xx . X),Y] in R;
A2: for m being Nat st m in Seg n holds
ex d being Element of Y st S₁[m,d]

proof

let m be Nat; :: thesis: ( m in Seg n implies ex d being Element of Y st S₁[m,d] )
assume m in Seg n ; :: thesis: ex d being Element of Y st S₁[m,d]
then reconsider mm = m as Element of Seg n ;
xxx . mm in dom R by A1;
then consider y being object such that
A3: [(xx . m),y] in R by XTUPLE_0:def 12;
reconsider yy = y as Element of Y by ZFMISC_1:87, A3;
take yy ; :: thesis: S₁[m,yy]
thus S₁[m,yy] by A3; :: thesis: verum

end;

consider f being FinSequence of Y such that
A4: ( len f = n & ( for m being Nat st m in Seg n holds
S₁[m,f /. m] ) ) from FINSEQ_4:sch 1(A2);
reconsider ff = f as Element of nn -tuples_on Y by FINSEQ_2:133, A4;
reconsider fff = ff as Element of Funcs ((Seg nn),Y) by FOMODEL0:11;
A5: dom fff = Seg nn by FUNCT_2:def 1;

now :: thesis: for j being set st j in Seg n holds
[(xx . j),(ff . j)] in R

let j be set ; :: thesis: ( j in Seg n implies [(xx . j),(ff . j)] in R )
assume A6: j in Seg n ; :: thesis: [(xx . j),(ff . j)] in R
then reconsider jj = j as Element of NAT ;
( jj in dom ff & S₁[jj,f /. jj] ) by A6, A4, A5;
hence [(xx . j),(ff . j)] in R by PARTFUN1:def 6; :: thesis: verum

end;

then [xx,ff] in n -placesOf R ;
hence x in dom (n -placesOf R) by XTUPLE_0:def 12; :: thesis: verum

end;

then ( n -tuples_on X c= dom (n -placesOf R) & dom (n -placesOf R) c= n -tuples_on X ) by TARSKI:def 3;
hence for b₁ being Relation of (n -tuples_on X),(n -tuples_on Y) st b₁ = n -placesOf R holds
b₁ is total by PARTFUN1:def 2, XBOOLE_0:def 10; :: thesis: verum