let n be Nat; :: thesis: for A being Subset of () st A is diophantine holds
A is recursively_enumerable

let A be Subset of (); :: thesis: ( A is diophantine implies A is recursively_enumerable )
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) \/ {()} 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 {()} c= INT by ZFMISC_1:31;
then (rng P0) \/ {()} c= INT by ;
then reconsider Q = q as INT -valued Polynomial of ((2 + n) + m),F_Real by ;
take m ; :: according to HILB10_5:def 4 :: thesis: ex P being INT -valued Polynomial of ((2 + n) + m),F_Real st
for X being n -element XFinSequence of NAT holds
( X in A iff 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 (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) )

take Q ; :: thesis: for X being n -element XFinSequence of NAT holds
( X in A iff 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 ) )

let X be n -element XFinSequence of NAT ; :: thesis: ( X in A iff 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 ) )

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: ( 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 ) implies X in A )
proof
assume X in A ; :: thesis: 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 )

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) \/ as non empty finite natural-membered set ;
reconsider a = max R as Element of NAT by ORDINAL1:def 12;
take a ; :: thesis: 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 )

let b be Element of NAT ; :: thesis: ( b <= a implies ex Y being m -element XFinSequence of NAT st
( ( for i being object st i in dom Y holds
Y . i <= a ) & eval (Q,(@ ((<%b,a%> ^ X) ^ Y))) = 0 ) )

assume b <= a ; :: thesis: ex Y being m -element XFinSequence of NAT st
( ( for i being object st i in dom Y holds
Y . i <= a ) & eval (Q,(@ ((<%b,a%> ^ X) ^ Y))) = 0 )

take y ; :: thesis: ( ( for i being object st i in dom y holds
y . i <= a ) & eval (Q,(@ ((<%b,a%> ^ X) ^ y))) = 0 )

thus for i being object st i in dom y holds
y . i <= a :: thesis: eval (Q,(@ ((<%b,a%> ^ X) ^ y))) = 0
proof
let i be object ; :: thesis: ( i in dom y implies y . i <= a )
assume i in dom y ; :: thesis: y . i <= a
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: verum
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) \/ as finite ext-real-membered set ;
A6: ( A | 0 = {} & {} = B | 0 ) ;
A7: ( (@ A) /^ 0 = @ A & @ A = A & A = S ^ (x ^ y) ) by ;
@ 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 ;
B = @ ((<%b,a%> ^ x) ^ y) by AFINSQ_1:27;
hence eval (Q,(@ ((<%b,a%> ^ X) ^ y))) = 0 by A5, A3, A6, A9; :: thesis: verum
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: X in A
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 ;
@ 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 ;
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: verum