let n be Nat; :: thesis: for a being Integer

for i1 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = a } is diophantine Subset of (n -xtuples_of NAT)

let a be Integer; :: thesis: for i1 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = a } is diophantine Subset of (n -xtuples_of NAT)

let i1 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = a } is diophantine Subset of (n -xtuples_of NAT)

set i2 = the Element of n;

defpred S_{1}[ XFinSequence of NAT ] means $1 . i1 = a;

defpred S_{2}[ XFinSequence of NAT ] means 1 * ($1 . i1) = (0 * ($1 . the Element of n)) + a;

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

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

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

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

for i1 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = a } is diophantine Subset of (n -xtuples_of NAT)

let a be Integer; :: thesis: for i1 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = a } is diophantine Subset of (n -xtuples_of NAT)

let i1 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = a } is diophantine Subset of (n -xtuples_of NAT)

set i2 = the Element of n;

defpred S

defpred S

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

( S

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

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