let n be Nat; :: thesis: for i1, i2 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = (p . i2) ! } is diophantine Subset of (n -xtuples_of NAT)
let i1, i2 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = (p . i2) ! } is diophantine Subset of (n -xtuples_of NAT)
set n6 = n + 6;
defpred S₁[ XFinSequence of NAT ] means $1 . i1 = ($1 . i2) ! ;
set RR = { p where p is n -element XFinSequence of NAT : S₁[p] } ;

per cases ( n = 0 or n <> 0 ) ;

suppose A1: n = 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = (p . i2) ! } is diophantine Subset of (n -xtuples_of NAT)

{ p where p is n -element XFinSequence of NAT : S₁[p] } c= n -xtuples_of NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { p where p is n -element XFinSequence of NAT : S₁[p] } or x in n -xtuples_of NAT )
assume x in { p where p is n -element XFinSequence of NAT : S₁[p] } ; :: thesis: x in n -xtuples_of NAT
then ex p being n -element XFinSequence of NAT st
( x = p & S₁[p] ) ;
hence x in n -xtuples_of NAT by HILB10_2:def 5; :: thesis: verum

end;

hence { p where p is n -element XFinSequence of NAT : p . i1 = (p . i2) ! } is diophantine Subset of (n -xtuples_of NAT) by A1; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = (p . i2) ! } is diophantine Subset of (n -xtuples_of NAT)

hence { p where p is n -element XFinSequence of NAT : p . i1 = (p . i2) ! } is diophantine Subset of (n -xtuples_of NAT) by Th31; :: thesis: verum

end;

end;