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 * (p . i3)) } 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 * (p . i3)) } is diophantine Subset of ()
let i1, i2, i3 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : a * (p . i1) < (b * (p . i2)) + (c * (p . i3)) } is diophantine Subset of ()
defpred S1[ Nat, Nat, Integer] means (a * \$1) + 0 < \$3;
deffunc H1( Nat, Nat, Nat) -> set = ((b * \$2) + (c * \$3)) + 0;
defpred S2[ XFinSequence of NAT ] means (a * (\$1 . i1)) + 0 < ((b * (\$1 . i2)) + (c * (\$1 . i3))) + 0;
defpred S3[ XFinSequence of NAT ] means a * (\$1 . i1) < (b * (\$1 . i2)) + (c * (\$1 . i3));
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 Th7;
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 Th11;
A3: 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 A4: for p being n -element XFinSequence of NAT holds
( S2[p] iff S3[p] ) ;
{ p where p is n -element XFinSequence of NAT : S2[p] } = { q where q is n -element XFinSequence of NAT : S3[q] } from hence { p where p is n -element XFinSequence of NAT : a * (p . i1) < (b * (p . i2)) + (c * (p . i3)) } is diophantine Subset of () by A3; :: thesis: verum