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;

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 total
by PARTFUN1:def 2, XBOOLE_0:def 10; :: thesis: verum

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)

then
( n -tuples_on X c= dom (n -placesOf R) & dom (n -placesOf R) c= n -tuples_on X )
by TARSKI:def 3;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_{1}[ 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_{1}[m,d]

A4: ( len f = n & ( for m being Nat st m in Seg n holds

S_{1}[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;

hence x in dom (n -placesOf R) by XTUPLE_0:def 12; :: thesis: verum

end;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

A2: for m being Nat st m in Seg n holds

ex d being Element of Y st S

proof

consider f being FinSequence of Y such that
let m be Nat; :: thesis: ( m in Seg n implies ex d being Element of Y st S_{1}[m,d] )

assume m in Seg n ; :: thesis: ex d being Element of Y st S_{1}[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_{1}[m,yy]

thus S_{1}[m,yy]
by A3; :: thesis: verum

end;assume m in Seg n ; :: thesis: ex d being Element of Y st S

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

thus S

A4: ( len f = n & ( for m being Nat st m in Seg n holds

S

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

then
[xx,ff] in n -placesOf R
;[(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_{1}[jj,f /. jj] )
by A6, A4, A5;

hence [(xx . j),(ff . j)] in R by PARTFUN1:def 6; :: thesis: verum

end;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

hence [(xx . j),(ff . j)] in R by PARTFUN1:def 6; :: thesis: verum

hence x in dom (n -placesOf R) by XTUPLE_0:def 12; :: thesis: verum

hence for b

b