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 (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 * (p . i3)) } is diophantine Subset of (n -xtuples_of NAT)
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 (n -xtuples_of NAT)
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 (n -xtuples_of NAT) by Th11;
A2: { p where p is n -element XFinSequence of NAT : S2[p] } is diophantine Subset of (n -xtuples_of NAT) by Th8;
{ p where p is n -element XFinSequence of NAT : ( S1[p] & S2[p] ) } is diophantine Subset of (n -xtuples_of NAT) from HILB10_3:sch 3(A1, A2);
 then A3: { p where p is n -element XFinSequence of NAT : S5[p] } is diophantine Subset of (n -xtuples_of NAT) ;
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 (n -xtuples_of NAT) by Th9;
A5: { p where p is n -element XFinSequence of NAT : S4[p] } is diophantine Subset of (n -xtuples_of NAT) by Th7;
{ p where p is n -element XFinSequence of NAT : ( S3[p] & S4[p] ) } is diophantine Subset of (n -xtuples_of NAT) from HILB10_3:sch 3(A4, A5);
 then A6: { p where p is n -element XFinSequence of NAT : S6[p] } is diophantine Subset of (n -xtuples_of NAT) ;
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 (n -xtuples_of NAT) from HILB10_3:sch 1(A3, A6);
 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 XREAL_1:48, XREAL_1:49;
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 HILB10_3:sch 2(A8);
 hence { p where p is n -element XFinSequence of NAT : a * (p . i1) = (b * (p . i2)) -' (c * (p . i3)) } is diophantine Subset of (n -xtuples_of NAT) by A7; :: thesis: verum