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 ()
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 ()
set n6 = n + 6;
defpred S1[ XFinSequence of NAT ] means \$1 . i1 = (\$1 . i2) ! ;
set RR = { p where p is n -element XFinSequence of NAT : S1[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 ()
{ p where p is n -element XFinSequence of NAT : S1[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 : S1[p] } or x in n -xtuples_of NAT )
assume x in { p where p is n -element XFinSequence of NAT : S1[p] } ; :: thesis:
then ex p being n -element XFinSequence of NAT st
( x = p & S1[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 () 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 ()
hence { p where p is n -element XFinSequence of NAT : p . i1 = (p . i2) ! } is diophantine Subset of () by Th31; :: thesis: verum
end;
end;