let n be Nat; :: thesis: for i being Element of n holds { p where p is n -element XFinSequence of NAT : p . i is prime } is diophantine Subset of (n -xtuples_of NAT)
let i be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : p . i is prime } is diophantine Subset of (n -xtuples_of NAT)
defpred S₁[ XFinSequence of NAT ] means $1 . i is prime ;
defpred S₂[ XFinSequence of NAT ] means ( (((($1 . i) -' 1) !) + 1) mod ($1 . i) = 0 & $1 . i > 1 );
A1: for q being n -element XFinSequence of NAT holds
( S₁[q] iff S₂[q] ) by NAT_5:22;
{ q where q is n -element XFinSequence of NAT : S₁[q] } = { r where r is n -element XFinSequence of NAT : S₂[r] } from HILB10_3:sch 2(A1);
hence { p where p is n -element XFinSequence of NAT : p . i is prime } is diophantine Subset of (n -xtuples_of NAT) by Th3; :: thesis: verum