let n be Nat; :: thesis:
let A be diophantine Subset of (n -xtuples_of NAT); :: thesis:
let k, nk be Nat; :: thesis:
assume A1: k + nk = n ; :: thesis:
consider nA being Nat, pA being INT -valued Polynomial of (n + nA),F_Real such that
A2: for s being object holds
( s in A iff ex x being n -element XFinSequence of NAT ex y being nA -element XFinSequence of NAT st
( s = x & eval (pA,(@ (x ^ y))) = 0 ) ) by HILB10_2:def 6;
dom (id (n + nA)) = n + nA ;
then reconsider I = id (n + nA) as XFinSequence by AFINSQ_1:5;
set I1 = I | nk;
set I2 = (I | n) /^ nk;
set I3 = I /^ n;
Segm nk c= Segm n by NAT_1:39, NAT_1:11, A1;
then A3: (I | n) | nk = I | nk by RELAT_1:74;
then A4: ( I = (I | n) ^ (I /^ n) & I | n = (I | nk) ^ ((I | n) /^ nk) ) ;
then A5: rng (I | n) misses rng (I /^ n) by HILB10_2:1;
A6: len I = n + nA ;
A7: n <= n + nA by NAT_1:11;
A8: ( len (I /^ n) = (n + nA) -' n & (n + nA) -' n = (n + nA) - n & len (I | n) = n ) by A6, AFINSQ_2:def 2, AFINSQ_1:54, NAT_1:11;
A9: ( len ((I | n) /^ nk) = n -' nk & n -' nk = n - nk & len (I | nk) = nk ) by A1, NAT_1:11, A8, AFINSQ_2:def 2, AFINSQ_1:54, A3;
A10: ( len ((((I | n) /^ nk) ^ (I | nk)) ^ (I /^ n)) = (len (((I | n) /^ nk) ^ (I | nk))) + (len (I /^ n)) & len (((I | n) /^ nk) ^ (I | nk)) = (len ((I | n) /^ nk)) + (len (I | nk)) ) by AFINSQ_1:17;
A11: rng (I | nk) misses rng ((I | n) /^ nk) by A4, HILB10_2:1;
A12: (rng (I | n)) \/ (rng (I /^ n)) = rng I by A4, AFINSQ_1:26;
A13: ( (rng (I | nk)) \/ (rng ((I | n) /^ nk)) = rng (I | n) & rng (((I | n) /^ nk) ^ (I | nk)) = (rng ((I | n) /^ nk)) \/ (rng (I | nk)) ) by A4, AFINSQ_1:26;
then rng ((((I | n) /^ nk) ^ (I | nk)) ^ (I /^ n)) = n + nA by A12, AFINSQ_1:26;
then reconsider J = (((I | n) /^ nk) ^ (I | nk)) ^ (I /^ n) as Function of (n + nA),(n + nA) by A10, A8, A9, FUNCT_2:1;
A14: J is onto by A13, A12, AFINSQ_1:26;
A15: ((I | n) /^ nk) ^ (I | nk) is one-to-one by A11, CARD_FIN:52;
J is one-to-one by A13, A5, A15, CARD_FIN:52;
then reconsider J = J as Permutation of (n + nA) by A14;
A16: J = (J ") " by FUNCT_1:43;
set h = pA permuted_by (J ");
reconsider H = pA permuted_by (J ") as Polynomial of (k + (nk + nA)),F_Real by A1;
( rng (pA permuted_by (J ")) = rng pA & rng pA c= INT ) by HILB10_2:26, RELAT_1:def 19;
then reconsider H = H as INT -valued Polynomial of (k + (nk + nA)),F_Real by RELAT_1:def 19;
set Y = { (p /^ nk) where p is n -element XFinSequence of NAT : p in A } ;
{ (p /^ nk) where p is n -element XFinSequence of NAT : p in A } c= k -xtuples_of NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in { (p /^ nk) where p is n -element XFinSequence of NAT : p in A } ; :: thesis:
then consider p being n -element XFinSequence of NAT such that
A17: ( y = p /^ nk & p in A ) ;
len p = n by CARD_1:def 7;
then p /^ nk is k -element by A1, A9, AFINSQ_2:def 2;
hence y in k -xtuples_of NAT by A17, HILB10_2:def 5; :: thesis:

end;

then reconsider Y = { (p /^ nk) where p is n -element XFinSequence of NAT : p in A } as Subset of (k -xtuples_of NAT) ;
for s being object holds
( s in Y iff ex x being k -element XFinSequence of NAT ex y being nk + nA -element XFinSequence of NAT st
( s = x & eval (H,(@ (x ^ y))) = 0 ) )

proof

let s be object ; :: thesis:
thus ( s in Y implies ex x being k -element XFinSequence of NAT ex y being nk + nA -element XFinSequence of NAT st
( s = x & eval (H,(@ (x ^ y))) = 0 ) ) :: thesis:

proof

assume s in Y ; :: thesis:
then consider w being n -element XFinSequence of NAT such that
A18: ( s = w /^ nk & w in A ) ;
consider x being n -element XFinSequence of NAT , y being nA -element XFinSequence of NAT such that
A19: ( w = x & eval (pA,(@ (x ^ y))) = 0 ) by A2, A18;
A20: eval (pA,(@ (x ^ y))) = eval ((pA permuted_by (J ")),((@ (x ^ y)) * ((J ") "))) by HILB10_2:25;
A21: ( len x = n & len y = nA ) by CARD_1:def 7;
then A22: len (x /^ nk) = k by A1, A9, AFINSQ_2:def 2;
x /^ nk is k -element by A21, A1, A9, AFINSQ_2:def 2;
then reconsider S = x /^ nk as k -element XFinSequence of NAT ;
A23: len (x | nk) = nk by CARD_1:def 7, A1;
reconsider XnkY = (x | nk) ^ y as nk + nA -element XFinSequence of NAT by A1;
A26: len (S ^ XnkY) = n + nA by A1, CARD_1:def 7;
A27: dom ((@ (x ^ y)) * J) = n + nA by FUNCT_2:def 1;
(x | nk) ^ (x /^ nk) = x ;
then A28: x ^ y = (x | nk) ^ (S ^ y) by AFINSQ_1:27;
for i being object st i in dom (S ^ XnkY) holds
((@ (x ^ y)) * J) . i = (S ^ XnkY) . i

proof

let j be object ; :: thesis:
assume A29: j in dom (S ^ XnkY) ; :: thesis:
then reconsider j = j as Nat ;
A30: ( j in dom J & ((@ (x ^ y)) * J) . j = (@ (x ^ y)) . (J . j) ) by A29, A26, A27, FUNCT_1:11, FUNCT_1:12;

per cases by A30, AFINSQ_1:20;

suppose A31: j in dom (((I | n) /^ nk) ^ (I | nk)) ; :: thesis:

then A32: J . j = (((I | n) /^ nk) ^ (I | nk)) . j by AFINSQ_1:def 3;

per cases by A31, AFINSQ_1:20;

suppose A33: j in dom ((I | n) /^ nk) ; :: thesis:

then A34: ( (((I | n) /^ nk) ^ (I | nk)) . j = ((I | n) /^ nk) . j & ((I | n) /^ nk) . j = (I | n) . (nk + j) & j < k ) by A9, A1, AFINSQ_2:def 2, AFINSQ_1:66, AFINSQ_1:def 3;
A35: nk + j in n by A1, A33, A9, AFINSQ_1:66, HILB10_3:3;
then A36: (I | n) . (nk + j) = I . (nk + j) by FUNCT_1:49;
A37: dom S c= dom (S ^ y) by AFINSQ_1:21;
A38: ( len S = k & k = len ((I | n) /^ nk) ) by CARD_1:def 7, A1, A9;
Segm n = n ;
then nk + j < n + nA by NAT_1:44, A35, A7, XXREAL_0:2;
then nk + j in Segm (n + nA) by NAT_1:44;
then ((@ (x ^ y)) * J) . j = (@ (x ^ y)) . (nk + j) by FUNCT_1:17, A32, A30, A36, A34
.= (x ^ y) . (nk + j) by HILB10_2:def 1
.= (S ^ y) . j by A23, A37, A22, A33, A1, A9, A28, AFINSQ_1:def 3
.= S . j by A22, A33, A1, A9, AFINSQ_1:def 3
.= (S ^ XnkY) . j by A33, A38, AFINSQ_1:def 3 ;
hence ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis:

end;

suppose ex k being Nat st
( k in dom (I | nk) & j = (len ((I | n) /^ nk)) + k ) ; :: thesis:

then consider w being Nat such that
A39: ( w in dom (I | nk) & j = (len ((I | n) /^ nk)) + w ) ;
A40: ( (((I | n) /^ nk) ^ (I | nk)) . j = (I | nk) . w & (I | nk) . w = I . w & w < nk ) by A39, A9, AFINSQ_1:66, AFINSQ_1:def 3, FUNCT_1:49;
A41: dom (x | nk) c= dom ((x | nk) ^ y) by AFINSQ_1:21;
nk <= nk + (k + nA) by NAT_1:11;
then w < n + nA by A1, A39, A9, AFINSQ_1:66, XXREAL_0:2;
then A42: w in Segm (n + nA) by NAT_1:44;
J . j = w by A42, A40, A32, FUNCT_1:17;
then ((@ (x ^ y)) * J) . j = ((x | nk) ^ (S ^ y)) . w by A30, A28, HILB10_2:def 1
.= (x | nk) . w by AFINSQ_1:def 3, A39, A23, A9
.= ((x | nk) ^ y) . w by A39, A23, A9, AFINSQ_1:def 3
.= (S ^ XnkY) . j by A22, A39, A1, A9, A41, A23, AFINSQ_1:def 3 ;
hence ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis:

end;

suppose ex n being Nat st
( n in dom (I /^ n) & j = (len (((I | n) /^ nk) ^ (I | nk))) + n ) ; :: thesis:

then consider w being Nat such that
A43: ( w in dom (I /^ n) & j = (len (((I | n) /^ nk) ^ (I | nk))) + w ) ;
A44: len (S ^ (x | nk)) = n by CARD_1:def 7, A1;
J . j = (I /^ n) . w by A43, AFINSQ_1:def 3
.= I . j by A9, A10, A43, AFINSQ_2:def 2
.= j by A29, A26, FUNCT_1:17 ;
then ((@ (x ^ y)) * J) . j = (x ^ y) . j by A30, HILB10_2:def 1
.= y . w by A9, A10, A43, A8, A21, AFINSQ_1:def 3
.= ((S ^ (x | nk)) ^ y) . j by A44, A9, A10, A43, A8, A21, AFINSQ_1:def 3
.= (S ^ XnkY) . j by AFINSQ_1:27 ;
hence ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis:

end;

then (@ (x ^ y)) * J = S ^ XnkY by CARD_1:def 7, A1, A27, FUNCT_1:2;
then (@ (x ^ y)) * J = @ (S ^ XnkY) by HILB10_2:def 1;
hence ex x being k -element XFinSequence of NAT ex y being nk + nA -element XFinSequence of NAT st
( s = x & eval (H,(@ (x ^ y))) = 0 ) by A19, A18, A20, A16; :: thesis:

end;

given S being k -element XFinSequence of NAT , XnkY being nk + nA -element XFinSequence of NAT such that A45: ( s = S & eval (H,(@ (S ^ XnkY))) = 0 ) ; :: thesis:
set Xnk = XnkY | nk;
set y = XnkY /^ nk;
set X = (XnkY | nk) ^ S;
A46: ( len S = k & len XnkY = nk + nA & nk + nA >= nk ) by NAT_1:11, CARD_1:def 7;
then A47: ( len (XnkY | nk) = nk & len (XnkY /^ nk) = (nk + nA) -' nk & (nk + nA) -' nk = (nk + nA) - nk ) by AFINSQ_1:54, AFINSQ_2:def 2;
reconsider y = XnkY /^ nk as nA -element XFinSequence of NAT by A47, CARD_1:def 7;
reconsider X = (XnkY | nk) ^ S as n -element XFinSequence of NAT by A1;
A48: X | nk = XnkY | nk by A47, AFINSQ_1:57;
(XnkY | nk) ^ S = (X | nk) ^ (X /^ nk) ;
then A49: X /^ nk = S by A48, AFINSQ_1:28;
A50: XnkY = (XnkY | nk) ^ y ;
A51: ( len X = n & len y = nA ) by CARD_1:def 7;
A52: len (X | nk) = nk by A47, AFINSQ_1:57;
A53: len (S ^ XnkY) = n + nA by CARD_1:def 7, A1;
A54: dom ((@ (X ^ y)) * J) = n + nA by FUNCT_2:def 1;
A55: X ^ y = (X | nk) ^ (S ^ y) by A48, AFINSQ_1:27;
for i being object st i in dom (S ^ XnkY) holds
((@ (X ^ y)) * J) . i = (S ^ XnkY) . i

proof

let j be object ; :: thesis:
assume A56: j in dom (S ^ XnkY) ; :: thesis:
then reconsider j = j as Nat ;
A57: ( j in dom J & ((@ (X ^ y)) * J) . j = (@ (X ^ y)) . (J . j) ) by A56, A53, A54, FUNCT_1:11, FUNCT_1:12;

per cases by A57, AFINSQ_1:20;

suppose A58: j in dom (((I | n) /^ nk) ^ (I | nk)) ; :: thesis:

then A59: J . j = (((I | n) /^ nk) ^ (I | nk)) . j by AFINSQ_1:def 3;

per cases by A58, AFINSQ_1:20;

suppose A60: j in dom ((I | n) /^ nk) ; :: thesis:

then A61: ( (((I | n) /^ nk) ^ (I | nk)) . j = ((I | n) /^ nk) . j & ((I | n) /^ nk) . j = (I | n) . (nk + j) & j < k ) by A9, A1, AFINSQ_2:def 2, AFINSQ_1:66, AFINSQ_1:def 3;
then A63: (I | n) . (nk + j) = I . (nk + j) by A1, HILB10_3:3, FUNCT_1:49;
A62: nk + j in n by A60, A1, HILB10_3:3, A9, AFINSQ_1:66;
A64: dom S c= dom (S ^ y) by AFINSQ_1:21;
A65: ( len S = k & k = len ((I | n) /^ nk) ) by CARD_1:def 7, A1, A9;
Segm n = n ;
then nk + j < n + nA by NAT_1:44, A62, A7, XXREAL_0:2;
then nk + j in Segm (n + nA) by NAT_1:44;
then I . (nk + j) = nk + j by FUNCT_1:17;
then ((@ (X ^ y)) * J) . j = ((X | nk) ^ (S ^ y)) . (nk + j) by A55, HILB10_2:def 1, A59, A57, A63, A61
.= (S ^ y) . j by A52, A64, A60, A1, A46, A9, AFINSQ_1:def 3
.= S . j by A60, A1, A46, A9, AFINSQ_1:def 3
.= (S ^ XnkY) . j by A60, A65, AFINSQ_1:def 3 ;
hence ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis:

end;

suppose ex k being Nat st
( k in dom (I | nk) & j = (len ((I | n) /^ nk)) + k ) ; :: thesis:

then consider w being Nat such that
A66: ( w in dom (I | nk) & j = (len ((I | n) /^ nk)) + w ) ;
A67: ( (((I | n) /^ nk) ^ (I | nk)) . j = (I | nk) . w & (I | nk) . w = I . w & w < nk ) by A66, A9, AFINSQ_1:66, AFINSQ_1:def 3, FUNCT_1:49;
A68: dom (X | nk) c= dom ((X | nk) ^ y) by AFINSQ_1:21;
nk <= nk + (k + nA) by NAT_1:11;
then w < n + nA by A1, A66, A9, AFINSQ_1:66, XXREAL_0:2;
then A69: w in Segm (n + nA) by NAT_1:44;
J . j = w by A59, A69, FUNCT_1:17, A67;
then ((@ (X ^ y)) * J) . j = (X ^ y) . w by HILB10_2:def 1, A57
.= (X | nk) . w by AFINSQ_1:def 3, A66, A52, A9, A55
.= ((X | nk) ^ y) . w by A66, A52, A9, AFINSQ_1:def 3
.= (S ^ XnkY) . j by A48, A46, A1, A9, A68, A47, A66, AFINSQ_1:def 3 ;
hence ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis:

end;

suppose ex n being Nat st
( n in dom (I /^ n) & j = (len (((I | n) /^ nk) ^ (I | nk))) + n ) ; :: thesis:

then consider w being Nat such that
A70: ( w in dom (I /^ n) & j = (len (((I | n) /^ nk) ^ (I | nk))) + w ) ;
A71: len (S ^ (X | nk)) = n by A1, CARD_1:def 7;
J . j = (I /^ n) . w by A70, AFINSQ_1:def 3
.= I . j by A9, A10, A70, AFINSQ_2:def 2
.= j by A56, A53, FUNCT_1:17 ;
then ((@ (X ^ y)) * J) . j = (X ^ y) . j by HILB10_2:def 1, A57
.= y . w by A9, A10, A70, A8, A51, AFINSQ_1:def 3
.= ((S ^ (X | nk)) ^ y) . j by A71, A9, A10, A70, A8, A51, AFINSQ_1:def 3
.= (S ^ XnkY) . j by AFINSQ_1:27, A48, A50 ;
hence ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis:

end;

then (@ (X ^ y)) * J = S ^ XnkY by CARD_1:def 7, A1, A54, FUNCT_1:2;
then (@ (X ^ y)) * J = @ (S ^ XnkY) by HILB10_2:def 1;
then eval (H,(@ (S ^ XnkY))) = eval (pA,(@ (X ^ y))) by A16, HILB10_2:25;
then X in A by A2, A45;
hence s in Y by A49, A45; :: thesis:

end;

hence { (p /^ nk) where p is n -element XFinSequence of NAT : p in A } is diophantine Subset of (k -xtuples_of NAT) by HILB10_2:def 6; :: thesis: