let n be Nat; :: thesis:
let A be Subset of (n -xtuples_of NAT); :: thesis:
assume A is diophantine ; :: thesis:
then consider m being Nat, P being INT -valued Polynomial of (n + m),F_Real such that
A1: for s being object holds
( s in A iff ex x being n -element XFinSequence of NAT ex y being m -element XFinSequence of NAT st
( s = x & eval (P,(@ (x ^ y))) = 0 ) ) by HILB10_2:def 6;
set nm = n + m;
reconsider P0 = P as INT -valued Polynomial of (0 + (n + m)),F_Real ;
consider q being Polynomial of ((0 + 2) + (n + m)),F_Real such that
A2: rng q c= (rng P0) \/ {(0. F_Real)} and
A3: for XY being Function of (0 + (n + m)),F_Real
for XanyY being Function of ((0 + 2) + (n + m)),F_Real st XY | 0 = XanyY | 0 & (@ XY) /^ 0 = (@ XanyY) /^ (0 + 2) holds
eval (P0,XY) = eval (q,XanyY) by HILB10_2:28;
A4: rng P0 c= INT by RELAT_1:def 19;
0. F_Real in INT by INT_1:def 1;
then {(0. F_Real)} c= INT by ZFMISC_1:31;
then (rng P0) \/ {(0. F_Real)} c= INT by A4, XBOOLE_1:8;
then reconsider Q = q as INT -valued Polynomial of ((2 + n) + m),F_Real by RELAT_1:def 19, A2, XBOOLE_1:1;
take m ; :: according to HILB10_5:def 4 :: thesis:
take Q ; :: thesis:
let X be n -element XFinSequence of NAT ; :: thesis:
reconsider S = <*> INT as 0 -element XFinSequence of NAT ;
thus ( X in A implies ex x being Element of NAT st
for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being object st i in dom Y holds
Y . i <= x ) & eval (Q,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) ) :: thesis:

proof

assume X in A ; :: thesis:
then consider x being n -element XFinSequence of NAT , y being m -element XFinSequence of NAT such that
A5: ( X = x & eval (P,(@ (x ^ y))) = 0 ) by A1;
reconsider R = (rng y) \/ {0} as non empty finite natural-membered set ;
reconsider a = max R as Element of NAT by ORDINAL1:def 12;
take a ; :: thesis:
let b be Element of NAT ; :: thesis:
assume b <= a ; :: thesis:
take y ; :: thesis:
thus for i being object st i in dom y holds
y . i <= a :: thesis:

proof

let i be object ; :: thesis:
assume i in dom y ; :: thesis:
then y . i in rng y by FUNCT_1:def 3;
then y . i in R by XBOOLE_0:def 3;
hence y . i <= a by XXREAL_2:def 8; :: thesis:

end;

reconsider A = @ (S ^ (x ^ y)) as Function of (0 + (n + m)),F_Real ;
reconsider B = @ ((S ^ <%b,a%>) ^ (x ^ y)) as Function of ((0 + 2) + (n + m)),F_Real ;
reconsider R = (rng y) \/ {0} as finite ext-real-membered set ;
A6: ( A | 0 = {} & {} = B | 0 ) ;
A7: ( (@ A) /^ 0 = @ A & @ A = A & A = S ^ (x ^ y) ) by AFINSQ_2:10, HILB10_2:def 1, HILB10_2:def 2;
@ B = B by HILB10_2:def 2;
then A8: @ B = (S ^ <%b,a%>) ^ (x ^ y) by HILB10_2:def 1;
len (S ^ <%b,a%>) = 0 + 2 by CARD_1:def 7;
then A9: (@ A) /^ 0 = (@ B) /^ (0 + 2) by A7, A8, AFINSQ_2:12;
B = @ ((<%b,a%> ^ x) ^ y) by AFINSQ_1:27;
hence eval (Q,(@ ((<%b,a%> ^ X) ^ y))) = 0 by A5, A3, A6, A9; :: thesis:

end;

given a being Element of NAT such that A10: for z being Element of NAT st z <= a holds
ex y being m -element XFinSequence of NAT st
( ( for i being object st i in dom y holds
y . i <= a ) & eval (Q,(@ ((<%z,a%> ^ X) ^ y))) = 0 ) ; :: thesis:
consider y being m -element XFinSequence of NAT such that
A11: ( ( for i being object st i in dom y holds
y . i <= a ) & eval (Q,(@ ((<%a,a%> ^ X) ^ y))) = 0 ) by A10;
reconsider C = @ (S ^ (X ^ y)) as Function of (0 + (n + m)),F_Real ;
reconsider B = @ ((S ^ <%a,a%>) ^ (X ^ y)) as Function of ((0 + 2) + (n + m)),F_Real ;
A12: ( C | 0 = {} & {} = B | 0 ) ;
A13: ( (@ C) /^ 0 = @ C & @ C = C & C = S ^ (X ^ y) ) by AFINSQ_2:10, HILB10_2:def 1, HILB10_2:def 2;
@ B = B by HILB10_2:def 2;
then A14: @ B = (S ^ <%a,a%>) ^ (X ^ y) by HILB10_2:def 1;
len (S ^ <%a,a%>) = 0 + 2 by CARD_1:def 7;
then A15: (@ C) /^ 0 = (@ B) /^ (0 + 2) by A13, A14, AFINSQ_2:12;
A16: B = @ ((<%a,a%> ^ X) ^ y) by AFINSQ_1:27;
eval (P,(@ (X ^ y))) = 0 by A11, A16, A3, A12, A15;
hence X in A by A1; :: thesis: