let n be Nat; :: thesis: for a, b, c being Integer
for i1, i2 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 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 i1, i2 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : a * (p . i1) <> (b * (p . i2)) + c } is diophantine Subset of ()
defpred S1[ XFinSequence of NAT ] means a * (\$1 . i1) > (b * (\$1 . i2)) + c;
defpred S2[ XFinSequence of NAT ] means (a * (\$1 . i1)) + (- c) < b * (\$1 . i2);
defpred S3[ XFinSequence of NAT ] means ( S1[\$1] or S2[\$1] );
defpred S4[ XFinSequence of NAT ] means a * (\$1 . i1) <> (b * (\$1 . i2)) + c;
A1: { p where p is n -element XFinSequence of NAT : S1[p] } is diophantine Subset of () by Th7;
A2: { p where p is n -element XFinSequence of NAT : S2[p] } is diophantine Subset of () by Th7;
A3: { p where p is n -element XFinSequence of NAT : ( S1[p] or S2[p] ) } is diophantine Subset of () from A4: for p being n -element XFinSequence of NAT holds
( S3[p] iff S4[p] )
proof
let p be n -element XFinSequence of NAT ; :: thesis: ( S3[p] iff S4[p] )
thus ( S3[p] implies S4[p] ) ; :: thesis: ( S4[p] implies S3[p] )
assume S4[p] ; :: thesis: S3[p]
then ( a * (p . i1) > (b * (p . i2)) + c or a * (p . i1) < (b * (p . i2)) + c ) by XXREAL_0:1;
then ( a * (p . i1) > (b * (p . i2)) + c or (a * (p . i1)) - c < b * (p . i2) ) by XREAL_1:19;
hence S3[p] ; :: thesis: verum
end;
{ p where p is n -element XFinSequence of NAT : S3[p] } = { q where q is n -element XFinSequence of NAT : S4[q] } from hence { p where p is n -element XFinSequence of NAT : a * (p . i1) <> (b * (p . i2)) + c } is diophantine Subset of () by A3; :: thesis: verum