let A be Subset of (n -xtuples_of NAT); ( A is empty implies A is diophantine )
assume A1:
A is empty
; A is diophantine
reconsider p = 1_ ((n + 0),F_Real) as INT -valued Polynomial of (n + 0),F_Real ;
take
0
; HILB10_2:def 6 ex p being INT -valued Polynomial of (n + 0),F_Real st
for s being object holds
( s in A iff ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st
( s = x & eval (p,(@ (x ^ y))) = 0 ) )
take
p
; for s being object holds
( s in A iff ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st
( s = x & eval (p,(@ (x ^ y))) = 0 ) )
let s be object ; ( s in A iff ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st
( s = x & eval (p,(@ (x ^ y))) = 0 ) )
thus
( s in A implies ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st
( s = x & eval (p,(@ (x ^ y))) = 0 ) )
by A1; ( ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st
( s = x & eval (p,(@ (x ^ y))) = 0 ) implies s in A )
given x being n -element XFinSequence of NAT , y being 0 -element XFinSequence of NAT such that A2:
( s = x & eval (p,(@ (x ^ y))) = 0 )
; s in A
eval (p,(@ (x ^ y))) =
1. F_Real
by POLYNOM2:21
.=
1
;
hence
s in A
by A2; verum