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

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 ) )

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

then reconsider D = { (p | k) where p is n -element XFinSequence of NAT : p in A } as Subset of (k -xtuples_of NAT) ;
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;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

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

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
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 )

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;( 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

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
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;( 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

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