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;

let x be object ; :: thesis:
assume x in n -tuples_on X ; :: thesis:
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]

let m be Nat; :: thesis:
assume m in Seg n ; :: thesis:
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:
thus S₁[m,yy] by A3; :: thesis:

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;

let j be set ; :: thesis:
assume A6: j in Seg n ; :: thesis:
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:

end;

end;