let n be Nat; :: thesis: for a, b being Integer
for i1 being Element of n holds { p where p is n -element XFinSequence of NAT : a * (p . i1) = b } is diophantine Subset of (n -xtuples_of NAT)
let a, b be Integer; :: thesis: for i1 being Element of n holds { p where p is n -element XFinSequence of NAT : a * (p . i1) = b } is diophantine Subset of (n -xtuples_of NAT)
let i1 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : a * (p . i1) = b } is diophantine Subset of (n -xtuples_of NAT)
set i2 = the Element of n;
defpred S₁[ XFinSequence of NAT ] means a * ($1 . i1) = b;
defpred S₂[ XFinSequence of NAT ] means a * ($1 . i1) = (0 * ($1 . the Element of n)) + b;
A1: for p being n -element XFinSequence of NAT holds
( S₁[p] iff S₂[p] ) ;
{ p where p is n -element XFinSequence of NAT : S₁[p] } = { q where q is n -element XFinSequence of NAT : S₂[q] } from HILB10_3:sch 2(A1);
hence { p where p is n -element XFinSequence of NAT : a * (p . i1) = b } is diophantine Subset of (n -xtuples_of NAT) by Th6; :: thesis: verum