let n be Nat; :: thesis: for i being Element of n holds { p where p is n -element XFinSequence of NAT : p . i > 1 } 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 > 1 } is diophantine Subset of (n -xtuples_of NAT)

defpred S_{1}[ XFinSequence of NAT ] means 1 * ($1 . i) > (0 * ($1 . i)) + 1;

defpred S_{2}[ XFinSequence of NAT ] means $1 . i > 1;

A1: for q being n -element XFinSequence of NAT holds

( S_{1}[q] iff S_{2}[q] )
;

{ q where q is n -element XFinSequence of NAT : S_{1}[q] } = { r where r is n -element XFinSequence of NAT : S_{2}[r] }
from HILB10_3:sch 2(A1);

hence { p where p is n -element XFinSequence of NAT : p . i > 1 } is diophantine Subset of (n -xtuples_of NAT) by HILB10_3:7; :: thesis: verum

let i be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : p . i > 1 } is diophantine Subset of (n -xtuples_of NAT)

defpred S

defpred S

A1: for q being n -element XFinSequence of NAT holds

( S

{ q where q is n -element XFinSequence of NAT : S

hence { p where p is n -element XFinSequence of NAT : p . i > 1 } is diophantine Subset of (n -xtuples_of NAT) by HILB10_3:7; :: thesis: verum