reconsider p = 0_ ((n + 0),F_Real) as INT -valued Polynomial of (n + 0),F_Real ;
set ALL = [#] (n -xtuples_of NAT);
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 [#] (n -xtuples_of NAT) 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 [#] (n -xtuples_of NAT) 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 [#] (n -xtuples_of NAT) 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 [#] (n -xtuples_of NAT) 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 ) ) :: 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 [#] (n -xtuples_of NAT) )

proof

assume s in [#] (n -xtuples_of NAT) ; :: 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 )
then reconsider x = s as NAT -valued n -element XFinSequence ;
set y = the 0 -element XFinSequence of NAT ;
eval (p,(@ (x ^ the 0 -element XFinSequence of NAT ))) = 0. F_Real by POLYNOM2:20
.= 0 ;
hence ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st
( s = x & eval (p,(@ (x ^ y))) = 0 ) ; :: thesis: verum

end;

given x being n -element XFinSequence of NAT , y being 0 -element XFinSequence of NAT such that A3: ( s = x & eval (p,(@ (x ^ y))) = 0 ) ; :: thesis: s in [#] (n -xtuples_of NAT)
thus s in [#] (n -xtuples_of NAT) by A3, Def5; :: thesis: verum