let n be Nat; :: thesis: for A being diophantine Subset of ()
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 ()

let A be diophantine Subset of (); :: 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 ()

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 () )
assume A1: k <= n ; :: thesis: { (p | k) 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;
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:
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 ;
then p | k is k -element by CARD_1:def 7;
hence y in k -xtuples_of NAT by ; :: thesis: verum
end;
then reconsider D = { (p | k) where p is n -element XFinSequence of NAT : p in A } as Subset of () ;
reconsider nk = n - k as Nat by ;
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 ;
len (x /^ k) = (k + nk) -' k by
.= nk by NAT_D:34 ;
then len ((x /^ k) ^ y) = nk + nA by ;
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 ;
reconsider xk = x | k as k -element XFinSequence of NAT by ;
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 ;
A14: len (y /^ nk) = (nk + nA) -' nk by
.= nA by NAT_D:34 ;
len (x ^ (y | nk)) = k + nk by ;
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 ;
x ^ y = X ^ Y by ;
then X in A by ;
then X | k in D ;
hence s in D by ; :: thesis: verum
end;
hence { (p | k) where p is n -element XFinSequence of NAT : p in A } is diophantine Subset of () by HILB10_2:def 6; :: thesis: verum