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[ XFinSequence of NAT ] means a * (\$1 . i1) = ((b * (\$1 . i2)) + ((- c) * (\$1 . i3))) + 0;
defpred S2[ XFinSequence of NAT ] means b * (\$1 . i2) >= (c * (\$1 . i3)) + 0;
defpred S3[ XFinSequence of NAT ] means a * (\$1 . i1) = (0 * (\$1 . i2)) * (\$1 . i3);
defpred S4[ XFinSequence of NAT ] means (b * (\$1 . i2)) + 0 < c * (\$1 . i3);
defpred S5[ XFinSequence of NAT ] means ( S1[\$1] & S2[\$1] );
A1: { p where p is n -element XFinSequence of NAT : S1[p] } is diophantine Subset of () by Th11;
A2: { p where p is n -element XFinSequence of NAT : S2[p] } is diophantine Subset of () by Th8;
{ p where p is n -element XFinSequence of NAT : ( S1[p] & S2[p] ) } is diophantine Subset of () from then A3: { p where p is n -element XFinSequence of NAT : S5[p] } is diophantine Subset of () ;
defpred S6[ XFinSequence of NAT ] means ( S3[\$1] & S4[\$1] );
A4: { p where p is n -element XFinSequence of NAT : S3[p] } is diophantine Subset of () by Th9;
A5: { p where p is n -element XFinSequence of NAT : S4[p] } is diophantine Subset of () by Th7;
{ p where p is n -element XFinSequence of NAT : ( S3[p] & S4[p] ) } is diophantine Subset of () from then A6: { p where p is n -element XFinSequence of NAT : S6[p] } is diophantine Subset of () ;
defpred S7[ XFinSequence of NAT ] means ( S5[\$1] or S6[\$1] );
defpred S8[ XFinSequence of NAT ] means a * (\$1 . i1) = (b * (\$1 . i2)) -' (c * (\$1 . i3));
A7: { p where p is n -element XFinSequence of NAT : ( S5[p] or S6[p] ) } is diophantine Subset of () from A8: for p being n -element XFinSequence of NAT holds
( S7[p] iff S8[p] )
proof
let p be n -element XFinSequence of NAT ; :: thesis: ( S7[p] iff S8[p] )
thus ( S7[p] implies S8[p] ) :: thesis: ( S8[p] implies S7[p] )
proof
assume S7[p] ; :: thesis: S8[p]
then ( ( a * (p . i1) = ((b * (p . i2)) + ((- c) * (p . i3))) + 0 & (b * (p . i2)) - (c * (p . i3)) >= 0 ) or ( a * (p . i1) = (0 * (p . i2)) * (p . i3) & (b * (p . i2)) - (c * (p . i3)) < 0 ) ) by ;
hence S8[p] by XREAL_0:def 2; :: thesis: verum
end;
assume S8[p] ; :: thesis: S7[p]
then ( ( a * (p . i1) = ((b * (p . i2)) - (c * (p . i3))) + 0 & (b * (p . i2)) - (c * (p . i3)) >= 0 ) or ( a * (p . i1) = 0 & (b * (p . i2)) - (c * (p . i3)) < 0 ) ) by XREAL_0:def 2;
hence S7[p] by XREAL_1:48, XREAL_1:49; :: thesis: verum
end;
{ p where p is n -element XFinSequence of NAT : S7[p] } = { q where q is n -element XFinSequence of NAT : S8[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 A7; :: thesis: verum