let n be Nat; :: thesis: for A being diophantine Subset of (n -xtuples_of NAT)
for k being Nat st k <= n holds
{ (p | k) 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 being Nat st k <= n holds
{ (p | k) where p is n -element XFinSequence of NAT : p in A } is diophantine Subset of (k -xtuples_of NAT)
let k be Nat; :: thesis: ( k <= n implies { (p | k) where p is n -element XFinSequence of NAT : p in A } is diophantine Subset of (k -xtuples_of NAT) )
assume A1: k <= n ; :: thesis: { (p | k) 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;
set D = { (p | k) where p is n -element XFinSequence of NAT : p in A } ;
{ (p | k) 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 | k) where p is n -element XFinSequence of NAT : p in A } or y in k -xtuples_of NAT )
assume y in { (p | k) where p is n -element XFinSequence of NAT : p in A } ; :: thesis: y in k -xtuples_of NAT
then consider p being n -element XFinSequence of NAT such that
A3: ( y = p | k & p in A ) ;
len p = n by CARD_1:def 7;
then len (p | k) = k by A1, AFINSQ_1:54;
then p | k is k -element by CARD_1:def 7;
hence y in k -xtuples_of NAT by A3, HILB10_2:def 5; :: thesis: verum

end;

then reconsider D = { (p | k) where p is n -element XFinSequence of NAT : p in A } as Subset of (k -xtuples_of NAT) ;
reconsider nk = n - k as Nat by A1, NAT_1:21;
reconsider P = pA as INT -valued Polynomial of (k + (nk + nA)),F_Real ;
for s being object holds
( s in D iff ex x being k -element XFinSequence of NAT ex y being nk + nA -element XFinSequence of NAT st
( s = x & eval (P,(@ (x ^ y))) = 0 ) )

proof

let s be object ; :: thesis: ( s in D iff ex x being k -element XFinSequence of NAT ex y being nk + nA -element XFinSequence of NAT st
( s = x & eval (P,(@ (x ^ y))) = 0 ) )
thus ( s in D implies ex x being k -element XFinSequence of NAT ex y being nk + nA -element XFinSequence of NAT st
( s = x & eval (P,(@ (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 (P,(@ (x ^ y))) = 0 ) implies s in D )

proof

assume s in D ; :: thesis: ex x being k -element XFinSequence of NAT ex y being nk + nA -element XFinSequence of NAT st
( s = x & eval (P,(@ (x ^ y))) = 0 )
then consider p being n -element XFinSequence of NAT such that
A4: ( s = p | k & p in A ) ;
consider x being n -element XFinSequence of NAT , y being nA -element XFinSequence of NAT such that
A5: ( p = x & eval (pA,(@ (x ^ y))) = 0 ) by A4, A2;
A6: x = (x | k) ^ (x /^ k) ;
A7: ( len x = n & len y = nA ) by CARD_1:def 7;
then A8: len (x | k) = k by A1, AFINSQ_1:54;
len (x /^ k) = (k + nk) -' k by A7, AFINSQ_2:def 2
.= nk by NAT_D:34 ;
then len ((x /^ k) ^ y) = nk + nA by A7, AFINSQ_1:17;
then reconsider X = (x /^ k) ^ y as nk + nA -element XFinSequence of NAT by CARD_1:def 7;
A9: x ^ y = (x | k) ^ X by A6, AFINSQ_1:27;
reconsider xk = x | k as k -element XFinSequence of NAT by A8, CARD_1:def 7;
s = xk by A4, A5;
hence ex x being k -element XFinSequence of NAT ex y being nk + nA -element XFinSequence of NAT st
( s = x & eval (P,(@ (x ^ y))) = 0 ) by A9, A5; :: thesis: verum

end;

given x being k -element XFinSequence of NAT , y being nk + nA -element XFinSequence of NAT such that A10: ( s = x & eval (P,(@ (x ^ y))) = 0 ) ; :: thesis: s in D
A11: y = (y | nk) ^ (y /^ nk) ;
A12: ( len x = k & len y = nk + nA ) by CARD_1:def 7;
then A13: len (y | nk) = nk by NAT_1:11, AFINSQ_1:54;
A14: len (y /^ nk) = (nk + nA) -' nk by A12, AFINSQ_2:def 2
.= nA by NAT_D:34 ;
len (x ^ (y | nk)) = k + nk by A12, A13, AFINSQ_1:17;
then reconsider X = x ^ (y | nk) as n -element XFinSequence of NAT by CARD_1:def 7;
reconsider Y = y /^ nk as nA -element XFinSequence of NAT by CARD_1:def 7, A14;
x ^ y = X ^ Y by A11, AFINSQ_1:27;
then X in A by A2, A10;
then X | k in D ;
hence s in D by A10, A12, AFINSQ_1:57; :: thesis: verum

end;

hence { (p | k) 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