let n, k be Nat; :: thesis:
let P be INT -valued Polynomial of k,F_Real; :: thesis:
let a be Integer; :: thesis:
let perm be Permutation of n; :: thesis:
let i1 be Element of n; :: thesis:
assume A1: k <= n ; :: thesis:
defpred S₁[ XFinSequence of NAT ] means for q being k -element XFinSequence of NAT st q = ($1 * perm) | k holds
a * ($1 . i1) = eval (P,(@ q));
set A = { p where p is n -element XFinSequence of NAT : S₁[p] } ;
{ p where p is n -element XFinSequence of NAT : S₁[p] } c= n -xtuples_of NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: y in { p where p is n -element XFinSequence of NAT : S₁[p] } ; :: thesis:
ex p being n -element XFinSequence of NAT st
( y = p & S₁[p] ) by A2;
hence y in n -xtuples_of NAT by HILB10_2:def 5; :: thesis:

end;

then reconsider A = { p where p is n -element XFinSequence of NAT : S₁[p] } as Subset of (n -xtuples_of NAT) ;

per cases ;

suppose n = 0 ; :: thesis:

then A is diophantine ;
hence { p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds
a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT) ; :: thesis:

end;

suppose A3: n <> 0 ; :: thesis:

reconsider nk = n - k as Nat by A1, NAT_1:21;
consider Q being Polynomial of (k + nk),F_Real such that
A4: rng Q c= (rng P) \/ {(0. F_Real)} and
A5: for x being Function of k,F_Real
for y being Function of (k + nk),F_Real st y | k = x holds
eval (P,x) = eval (Q,y) by HILB10_2:27;
A6: rng P c= INT by RELAT_1:def 19;
0. F_Real in INT by INT_1:def 1;
then {(0. F_Real)} c= INT by ZFMISC_1:31;
then (rng P) \/ {(0. F_Real)} c= INT by A6, XBOOLE_1:8;
then reconsider Q1 = Q as INT -valued Polynomial of n,F_Real by RELAT_1:def 19, A4, XBOOLE_1:1;
set T = Q1 permuted_by perm;
A7: rng (Q1 permuted_by perm) = rng Q1 by HILB10_2:26;
rng Q1 c= INT by RELAT_1:def 19;
then reconsider T1 = Q1 permuted_by perm as INT -valued Polynomial of n,F_Real by A7, RELAT_1:def 19;
reconsider FR = F_Real as Field ;
reconsider ar = a as Element of FR by XREAL_0:def 1;
reconsider Ar = ar as Element of F_Real ;
reconsider t = Q1 permuted_by perm as Polynomial of n,FR ;
T1 = t ;
then reconsider TI = t - (ar * (1_1 (i1,FR))) as INT -valued Polynomial of (n + 0),F_Real ;
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 (TI,(@ (x ^ y))) = 0 ) )

proof

let s be object ; :: thesis:
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 (TI,(@ (x ^ y))) = 0 ) ) :: thesis:

proof

assume s in A ; :: thesis:
then consider p being n -element XFinSequence of NAT such that
A8: ( s = p & S₁[p] ) ;
reconsider E = <%> NAT as 0 -element XFinSequence of NAT ;
take p ; :: thesis:
take E ; :: thesis:
thus s = p by A8; :: thesis:
reconsider pE = @ (p ^ E) as Function of n,FR ;
A9: eval ((1_1 (i1,FR)),pE) = pE . i1 by A3, HILB10_3:1
.= p . i1 by HILB10_2:def 1 ;
reconsider Eval = eval ((1_1 (i1,FR)),pE) as Element of F_Real ;
A10: eval ((ar * (1_1 (i1,FR))),pE) = Ar * Eval by POLYNOM7:29
.= a * (p . i1) by A9 ;
A11: ( dom perm = n & rng perm = n & len p = n ) by FUNCT_2:52, FUNCT_2:def 3, CARD_1:def 7;
then dom (p * perm) = n by RELAT_1:27;
then reconsider pp = p * perm as XFinSequence by AFINSQ_1:5;
A12: len pp = n by A11, RELAT_1:27;
reconsider PP = pp as n -element XFinSequence of NAT by A12, CARD_1:def 7;
len (PP | k) = k by A12, A1, AFINSQ_1:54;
then reconsider PPk = PP | k as k -element XFinSequence of NAT by CARD_1:def 7;
(@ PP) | k = PP | k by HILB10_2:def 1;
then A13: (@ PP) | k = @ PPk by HILB10_2:def 1;
PP * (perm ") = p * (perm * (perm ")) by RELAT_1:36
.= p * (id n) by FUNCT_2:61
.= p by A11, RELAT_1:51 ;
then A14: PP * (perm ") = @ p by HILB10_2:def 1;
A15: eval ((Q1 permuted_by perm),(@ p)) = eval ((Q1 permuted_by perm),((@ PP) * (perm "))) by A14, HILB10_2:def 1
.= eval (Q1,(@ PP)) by HILB10_2:25
.= eval (P,(@ PPk)) by A5, A13
.= a * (p . i1) by A8 ;
thus eval (TI,(@ (p ^ E))) = (eval (t,pE)) - (eval ((ar * (1_1 (i1,FR))),pE)) by POLYNOM2:24
.= 0. FR by A10, A15, RLVECT_1:5
.= 0 ; :: thesis:

end;

given x being n -element XFinSequence of NAT , y being 0 -element XFinSequence of NAT such that A16: ( s = x & eval (TI,(@ (x ^ y))) = 0 ) ; :: thesis:
reconsider xy = @ (x ^ y) as Function of n,FR ;
A17: eval ((1_1 (i1,FR)),xy) = xy . i1 by A3, HILB10_3:1
.= x . i1 by HILB10_2:def 1 ;
reconsider Eval = eval ((1_1 (i1,FR)),xy) as Element of F_Real ;
A18: eval ((ar * (1_1 (i1,FR))),xy) = Ar * Eval by POLYNOM7:29
.= a * (x . i1) by A17 ;
A19: ( dom perm = n & rng perm = n & len x = n ) by FUNCT_2:52, FUNCT_2:def 3, CARD_1:def 7;
then dom (x * perm) = n by RELAT_1:27;
then reconsider xp = x * perm as XFinSequence by AFINSQ_1:5;
A20: len xp = n by A19, RELAT_1:27;
reconsider XP = xp as n -element XFinSequence of NAT by A20, CARD_1:def 7;
len (XP | k) = k by A20, A1, AFINSQ_1:54;
then reconsider XPk = XP | k as k -element XFinSequence of NAT by CARD_1:def 7;
(@ XP) | k = XP | k by HILB10_2:def 1;
then A21: (@ XP) | k = @ XPk by HILB10_2:def 1;
XP * (perm ") = x * (perm * (perm ")) by RELAT_1:36
.= x * (id n) by FUNCT_2:61
.= x by A19, RELAT_1:51 ;
then A22: XP * (perm ") = @ x by HILB10_2:def 1;
A23: eval ((Q1 permuted_by perm),(@ x)) = eval ((Q1 permuted_by perm),((@ XP) * (perm "))) by A22, HILB10_2:def 1
.= eval (Q1,(@ XP)) by HILB10_2:25
.= eval (P,(@ XPk)) by A5, A21 ;
A24: (eval (t,xy)) - (eval ((ar * (1_1 (i1,FR))),xy)) = 0. FR by POLYNOM2:24, A16;
S₁[x] by A24, A18, A23, VECTSP_1:19;
hence s in A by A16; :: thesis:

end;

hence { p where p is n -element XFinSequence of NAT : for q being k -element XFinSequence of NAT st q = (p * perm) | k holds
a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT) by HILB10_2:def 6; :: thesis:

end;