let n, k be Nat; :: thesis: for P being INT -valued Polynomial of k,F_Real
for a being Integer
for perm being Permutation of n
for i1 being Element of n st k <= n holds
{ 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 ()

let P be INT -valued Polynomial of k,F_Real; :: thesis: for a being Integer
for perm being Permutation of n
for i1 being Element of n st k <= n holds
{ 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 ()

let a be Integer; :: thesis: for perm being Permutation of n
for i1 being Element of n st k <= n holds
{ 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 ()

let perm be Permutation of n; :: thesis: for i1 being Element of n st k <= n holds
{ 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 ()

let i1 be Element of n; :: thesis: ( k <= n implies { 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 () )

assume A1: k <= n ; :: thesis: { 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 ()

defpred S1[ 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 : S1[p] } ;
{ p where p is n -element XFinSequence of NAT : S1[p] } c= n -xtuples_of NAT
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { p where p is n -element XFinSequence of NAT : S1[p] } or y in n -xtuples_of NAT )
assume A2: y in { p where p is n -element XFinSequence of NAT : S1[p] } ; :: thesis:
ex p being n -element XFinSequence of NAT st
( y = p & S1[p] ) by A2;
hence y in n -xtuples_of NAT by HILB10_2:def 5; :: thesis: verum
end;
then reconsider A = { p where p is n -element XFinSequence of NAT : S1[p] } as Subset of () ;
per cases ( n = 0 or n <> 0 ) ;
suppose n = 0 ; :: thesis: { 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 ()

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 () ; :: thesis: verum
end;
suppose A3: n <> 0 ; :: thesis: { 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 ()

reconsider nk = n - k as Nat by ;
consider Q being Polynomial of (k + nk),F_Real such that
A4: rng Q c= (rng P) \/ {()} 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 {()} c= INT by ZFMISC_1:31;
then (rng P) \/ {()} c= INT by ;
then reconsider Q1 = Q as INT -valued Polynomial of n,F_Real by ;
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 ;
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: ( 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 ) )

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: ( ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st
( s = x & eval (TI,(@ (x ^ y))) = 0 ) implies s in A )
proof
assume s in A ; :: thesis: ex x being n -element XFinSequence of NAT ex y being 0 -element XFinSequence of NAT st
( s = x & eval (TI,(@ (x ^ y))) = 0 )

then consider p being n -element XFinSequence of NAT such that
A8: ( s = p & S1[p] ) ;
reconsider E = <%> NAT as 0 -element XFinSequence of NAT ;
take p ; :: thesis: ex y being 0 -element XFinSequence of NAT st
( s = p & eval (TI,(@ (p ^ y))) = 0 )

take E ; :: thesis: ( s = p & eval (TI,(@ (p ^ E))) = 0 )
thus s = p by A8; :: thesis: eval (TI,(@ (p ^ E))) = 0
reconsider pE = @ (p ^ E) as Function of n,FR ;
A9: eval ((1_1 (i1,FR)),pE) = pE . i1 by
.= 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 ;
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 ;
reconsider PP = pp as n -element XFinSequence of NAT by ;
len (PP | k) = k by ;
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 ;
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
.= eval (Q1,(@ PP)) by HILB10_2:25
.= eval (P,(@ PPk)) by
.= 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
.= 0 ; :: thesis: verum
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: s in A
reconsider xy = @ (x ^ y) as Function of n,FR ;
A17: eval ((1_1 (i1,FR)),xy) = xy . i1 by
.= 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 ;
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 ;
reconsider XP = xp as n -element XFinSequence of NAT by ;
len (XP | k) = k by ;
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 ;
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
.= eval (Q1,(@ XP)) by HILB10_2:25
.= eval (P,(@ XPk)) by ;
A24: (eval (t,xy)) - (eval ((ar * (1_1 (i1,FR))),xy)) = 0. FR by ;
S1[x] by A24, A18, A23, VECTSP_1:19;
hence s in A by A16; :: thesis: verum
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 () by HILB10_2:def 6; :: thesis: verum
end;
end;