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

let A be Subset of (); :: thesis: ( A is recursively_enumerable implies A is diophantine )
assume A is recursively_enumerable ; :: thesis: A is diophantine
then consider m being Nat, P being INT -valued Polynomial of ((2 + n) + m),F_Real such that
A1: 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 ) ) ;
set X = { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 )
}
;
A2: A c= { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 )
}
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 )
}
)

assume A3: a in A ; :: thesis: a in { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 )
}

reconsider a = a as n -element XFinSequence of NAT by ;
consider x being Element of NAT such that
A4: 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%> ^ a) ^ Y))) = 0 ) by A3, A1;
now :: thesis: for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 )
let z be Element of NAT ; :: thesis: ( z <= x implies ex Y being m -element XFinSequence of NAT st
( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 ) )

assume A5: z <= x ; :: thesis: ex Y being m -element XFinSequence of NAT st
( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 )

consider Y being m -element XFinSequence of NAT such that
A6: ( ( for i being object st i in dom Y holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 ) by A4, A5;
take Y = Y; :: thesis: ( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 )

len Y = m by CARD_1:def 7;
hence ( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ a) ^ Y))) = 0 ) by A6; :: thesis: verum
end;
hence a in { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 )
}
; :: thesis: verum
end;
{ X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } c= A
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 )
}
or b in A )

assume A7: b in { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 )
}
; :: thesis: b in A
consider X being n -element XFinSequence of NAT such that
A8: ( b = X & 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 Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) ) by A7;
consider x being Element of NAT such that
A9: for z being Element of NAT st z <= x holds
ex Y being m -element XFinSequence of NAT st
( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) by A8;
now :: thesis: 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 )
let z be Element of NAT ; :: thesis: ( z <= x implies 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 ) )

assume A10: z <= x ; :: thesis: 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 )

consider Y being m -element XFinSequence of NAT such that
A11: ( ( for i being Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) by ;
take Y = Y; :: thesis: ( ( for i being object st i in dom Y holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 )

m = len Y by CARD_1:def 7;
hence ( ( for i being object st i in dom Y holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) by A11; :: thesis: verum
end;
hence b in A by A1, A8; :: thesis: verum
end;
then { X where X is n -element XFinSequence of NAT : 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 Nat st i in m holds
Y . i <= x ) & eval (P,(@ ((<%z,x%> ^ X) ^ Y))) = 0 ) } = A by ;
hence A is diophantine by Th19; :: thesis: verum