let n be Nat; :: thesis: for a, b, c being Integer

for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) -' c } is diophantine Subset of (n -xtuples_of NAT)

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

defpred S_{1}[ Nat, Nat, Integer] means a * $1 = (b * $2) -' $3;

A1: for n being Nat

for i1, i2, i3 being Element of n

for d being Integer holds { p where p is b_{1} -element XFinSequence of NAT : S_{1}[p . i1,p . i2,d * (p . i3)] } is diophantine Subset of (n -xtuples_of NAT)
by Th19;

deffunc H_{1}( Nat, Nat, Nat) -> Integer = c;

A2: for n being Nat

for i1, i2, i3, i4 being Element of n

for d being Integer holds { p where p is b_{1} -element XFinSequence of NAT : H_{1}(p . i1,p . i2,p . i3) = d * (p . i4) } is diophantine Subset of (n -xtuples_of NAT)
by Th13;

for n being Nat

for i1, i2, i3, i4, i5 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : S_{1}[p . i1,p . i2,H_{1}(p . i3,p . i4,p . i5)] } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 5(A1, A2);

hence for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) -' c } is diophantine Subset of (n -xtuples_of NAT) ; :: thesis: verum

for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) -' c } is diophantine Subset of (n -xtuples_of NAT)

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

defpred S

A1: for n being Nat

for i1, i2, i3 being Element of n

for d being Integer holds { p where p is b

deffunc H

A2: for n being Nat

for i1, i2, i3, i4 being Element of n

for d being Integer holds { p where p is b

for n being Nat

for i1, i2, i3, i4, i5 being Element of n holds { p where p is b

hence for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) -' c } is diophantine Subset of (n -xtuples_of NAT) ; :: thesis: verum