let n be Nat; :: thesis: for A being diophantine Subset of (n -xtuples_of NAT)
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 (k -xtuples_of NAT)
let A be diophantine Subset of (n -xtuples_of NAT); :: 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 (k -xtuples_of NAT)
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 (k -xtuples_of NAT) )
assume A1: k + nk = n ; :: thesis: { (p /^ nk) where p is n -element XFinSequence of NAT : p in A } is diophantine Subset of (k -xtuples_of NAT)
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 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 ) ) 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: verum