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 ()

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 ()
defpred S1[ 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 b1 -element XFinSequence of NAT : S1[p . i1,p . i2,d * (p . i3)] } is diophantine Subset of () by Th19;
deffunc H1( 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 b1 -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = d * (p . i4) } is diophantine Subset of () by Th13;
for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S1[p . i1,p . i2,H1(p . i3,p . i4,p . i5)] } is diophantine Subset of () from 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 () ; :: thesis: verum