let n be Nat; :: thesis: for A being diophantine Subset of ()
for k, nk being Nat st k + nk = n holds
{ (p /^ nk) where p is n -element XFinSequence of NAT : p in A } is diophantine Subset of ()

let A be diophantine Subset of (); :: thesis: for k, nk being Nat st k + nk = n holds
{ (p /^ nk) where p is n -element XFinSequence of NAT : p in A } is diophantine Subset of ()

let k, nk be Nat; :: thesis: ( k + nk = n implies { (p /^ nk) where p is n -element XFinSequence of NAT : p in A } is diophantine Subset of () )
assume A1: k + nk = n ; :: thesis: { (p /^ nk) where p is n -element XFinSequence of NAT : p in A } is diophantine Subset of ()
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 ;
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 ;
A9: ( len ((I | n) /^ nk) = n -' nk & n -' nk = n - nk & len (I | nk) = nk ) by ;
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 ;
A12: (rng (I | n)) \/ (rng (I /^ n)) = rng I by ;
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 ;
then rng ((((I | n) /^ nk) ^ (I | nk)) ^ (I /^ n)) = n + nA by ;
then reconsider J = (((I | n) /^ nk) ^ (I | nk)) ^ (I /^ n) as Function of (n + nA),(n + nA) by ;
A14: J is onto by ;
A15: ((I | n) /^ nk) ^ (I | nk) is one-to-one by ;
J is one-to-one by ;
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 ;
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: ( not y in { (p /^ nk) where p is n -element XFinSequence of NAT : p in A } or y in k -xtuples_of NAT )
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 ;
hence y in k -xtuples_of NAT by ; :: thesis: verum
end;
then reconsider Y = { (p /^ nk) where p is n -element XFinSequence of NAT : p in A } as Subset of () ;
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: ( 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 ) )

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: ( 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 ) implies s in Y )
proof
assume s in Y ; :: thesis: 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 )

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 ;
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 ;
x /^ nk is k -element by ;
then reconsider S = x /^ nk as k -element XFinSequence of NAT ;
A23: len (x | nk) = nk by ;
reconsider XnkY = (x | nk) ^ y as nk + nA -element XFinSequence of NAT by A1;
A26: len (S ^ XnkY) = n + nA by ;
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: ( j in dom (S ^ XnkY) implies ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j )
assume A29: j in dom (S ^ XnkY) ; :: thesis: ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j
then reconsider j = j as Nat ;
A30: ( j in dom J & ((@ (x ^ y)) * J) . j = (@ (x ^ y)) . (J . j) ) by ;
per cases ( j in dom (((I | n) /^ nk) ^ (I | nk)) or ex n being Nat st
( n in dom (I /^ n) & j = (len (((I | n) /^ nk) ^ (I | nk))) + n ) )
by ;
suppose A31: j in dom (((I | n) /^ nk) ^ (I | nk)) ; :: thesis: ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j
then A32: J . j = (((I | n) /^ nk) ^ (I | nk)) . j by AFINSQ_1:def 3;
per cases ( j in dom ((I | n) /^ nk) or ex k being Nat st
( k in dom (I | nk) & j = (len ((I | n) /^ nk)) + k ) )
by ;
suppose A33: j in dom ((I | n) /^ nk) ; :: thesis: ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j
then A34: ( (((I | n) /^ nk) ^ (I | nk)) . j = ((I | n) /^ nk) . j & ((I | n) /^ nk) . j = (I | n) . (nk + j) & j < k ) by ;
A35: nk + j in n by ;
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 ;
Segm n = n ;
then nk + j < n + nA by ;
then nk + j in Segm (n + nA) by NAT_1:44;
then ((@ (x ^ y)) * J) . j = (@ (x ^ y)) . (nk + j) by
.= (x ^ y) . (nk + j) by HILB10_2:def 1
.= (S ^ y) . j by
.= S . j by
.= (S ^ XnkY) . j by ;
hence ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum
end;
suppose ex k being Nat st
( k in dom (I | nk) & j = (len ((I | n) /^ nk)) + k ) ; :: thesis: ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j
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 ;
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 ;
then A42: w in Segm (n + nA) by NAT_1:44;
J . j = w by ;
then ((@ (x ^ y)) * J) . j = ((x | nk) ^ (S ^ y)) . w by
.= (x | nk) . w by
.= ((x | nk) ^ y) . w by
.= (S ^ XnkY) . j by ;
hence ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum
end;
end;
end;
suppose ex n being Nat st
( n in dom (I /^ n) & j = (len (((I | n) /^ nk) ^ (I | nk))) + n ) ; :: thesis: ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j
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 ;
J . j = (I /^ n) . w by
.= I . j by
.= j by ;
then ((@ (x ^ y)) * J) . j = (x ^ y) . j by
.= y . w by
.= ((S ^ (x | nk)) ^ y) . j by
.= (S ^ XnkY) . j by AFINSQ_1:27 ;
hence ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum
end;
end;
end;
then (@ (x ^ y)) * J = S ^ XnkY by ;
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: verum
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: s in Y
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 ;
then A47: ( len (XnkY | nk) = nk & len (XnkY /^ nk) = (nk + nA) -' nk & (nk + nA) -' nk = (nk + nA) - nk ) by ;
reconsider y = XnkY /^ nk as nA -element XFinSequence of NAT by ;
reconsider X = (XnkY | nk) ^ S as n -element XFinSequence of NAT by A1;
A48: X | nk = XnkY | nk by ;
(XnkY | nk) ^ S = (X | nk) ^ (X /^ nk) ;
then A49: X /^ nk = S by ;
A50: XnkY = (XnkY | nk) ^ y ;
A51: ( len X = n & len y = nA ) by CARD_1:def 7;
A52: len (X | nk) = nk by ;
A53: len (S ^ XnkY) = n + nA by ;
A54: dom ((@ (X ^ y)) * J) = n + nA by FUNCT_2:def 1;
A55: X ^ y = (X | nk) ^ (S ^ y) by ;
for i being object st i in dom (S ^ XnkY) holds
((@ (X ^ y)) * J) . i = (S ^ XnkY) . i
proof
let j be object ; :: thesis: ( j in dom (S ^ XnkY) implies ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j )
assume A56: j in dom (S ^ XnkY) ; :: thesis: ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j
then reconsider j = j as Nat ;
A57: ( j in dom J & ((@ (X ^ y)) * J) . j = (@ (X ^ y)) . (J . j) ) by ;
per cases ( j in dom (((I | n) /^ nk) ^ (I | nk)) or ex n being Nat st
( n in dom (I /^ n) & j = (len (((I | n) /^ nk) ^ (I | nk))) + n ) )
by ;
suppose A58: j in dom (((I | n) /^ nk) ^ (I | nk)) ; :: thesis: ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j
then A59: J . j = (((I | n) /^ nk) ^ (I | nk)) . j by AFINSQ_1:def 3;
per cases ( j in dom ((I | n) /^ nk) or ex k being Nat st
( k in dom (I | nk) & j = (len ((I | n) /^ nk)) + k ) )
by ;
suppose A60: j in dom ((I | n) /^ nk) ; :: thesis: ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j
then A61: ( (((I | n) /^ nk) ^ (I | nk)) . j = ((I | n) /^ nk) . j & ((I | n) /^ nk) . j = (I | n) . (nk + j) & j < k ) by ;
then A63: (I | n) . (nk + j) = I . (nk + j) by ;
A62: nk + j in n by ;
A64: dom S c= dom (S ^ y) by AFINSQ_1:21;
A65: ( len S = k & k = len ((I | n) /^ nk) ) by ;
Segm n = n ;
then nk + j < n + nA by ;
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
.= (S ^ y) . j by
.= S . j by
.= (S ^ XnkY) . j by ;
hence ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum
end;
suppose ex k being Nat st
( k in dom (I | nk) & j = (len ((I | n) /^ nk)) + k ) ; :: thesis: ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j
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 ;
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 ;
then A69: w in Segm (n + nA) by NAT_1:44;
J . j = w by ;
then ((@ (X ^ y)) * J) . j = (X ^ y) . w by
.= (X | nk) . w by
.= ((X | nk) ^ y) . w by
.= (S ^ XnkY) . j by ;
hence ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum
end;
end;
end;
suppose ex n being Nat st
( n in dom (I /^ n) & j = (len (((I | n) /^ nk) ^ (I | nk))) + n ) ; :: thesis: ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j
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 ;
J . j = (I /^ n) . w by
.= I . j by
.= j by ;
then ((@ (X ^ y)) * J) . j = (X ^ y) . j by
.= y . w by
.= ((S ^ (X | nk)) ^ y) . j by
.= (S ^ XnkY) . j by ;
hence ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum
end;
end;
end;
then (@ (X ^ y)) * J = S ^ XnkY by ;
then (@ (X ^ y)) * J = @ (S ^ XnkY) by HILB10_2:def 1;
then eval (H,(@ (S ^ XnkY))) = eval (pA,(@ (X ^ y))) by ;
then X in A by ;
hence s in Y by ; :: thesis: verum
end;
hence { (p /^ nk) where p is n -element XFinSequence of NAT : p in A } is diophantine Subset of () by HILB10_2:def 6; :: thesis: verum