let A be Subset of (n -xtuples_of NAT); :: thesis: ( A is empty implies A is diophantine )
assume A1: A is empty ; :: thesis: A is diophantine
reconsider p = 1_ ((n + 0),F_Real) as INT -valued Polynomial of (n + 0),F_Real ;
take 0 ; :: according to HILB10_2:def 6 :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: ( 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 ) ; :: thesis: s in A
eval (p,(@ (x ^ y))) = 1. F_Real by POLYNOM2:21
.= 1 ;
hence s in A by A2; :: thesis: verum