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

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

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

proof

then reconsider Y = { (p /^ nk) 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 /^ 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: y in k -xtuples_of NAT

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 A1, A9, AFINSQ_2:def 2;

hence y in k -xtuples_of NAT by A17, HILB10_2:def 5; :: thesis: verum

end;assume y in { (p /^ nk) 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

A17: ( y = p /^ nk & p in A ) ;

len p = n by CARD_1:def 7;

then p /^ nk is k -element by A1, A9, AFINSQ_2:def 2;

hence y in k -xtuples_of NAT by A17, HILB10_2:def 5; :: thesis: verum

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

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

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 NAT_1:11, CARD_1:def 7;

then A47: ( len (XnkY | nk) = nk & len (XnkY /^ nk) = (nk + nA) -' nk & (nk + nA) -' nk = (nk + nA) - nk ) by AFINSQ_1:54, AFINSQ_2:def 2;

reconsider y = XnkY /^ nk as nA -element XFinSequence of NAT by A47, CARD_1:def 7;

reconsider X = (XnkY | nk) ^ S as n -element XFinSequence of NAT by A1;

A48: X | nk = XnkY | nk by A47, AFINSQ_1:57;

(XnkY | nk) ^ S = (X | nk) ^ (X /^ nk) ;

then A49: X /^ nk = S by A48, AFINSQ_1:28;

A50: XnkY = (XnkY | nk) ^ y ;

A51: ( len X = n & len y = nA ) by CARD_1:def 7;

A52: len (X | nk) = nk by A47, AFINSQ_1:57;

A53: len (S ^ XnkY) = n + nA by CARD_1:def 7, A1;

A54: dom ((@ (X ^ y)) * J) = n + nA by FUNCT_2:def 1;

A55: X ^ y = (X | nk) ^ (S ^ y) by A48, AFINSQ_1:27;

for i being object st i in dom (S ^ XnkY) holds

((@ (X ^ y)) * J) . i = (S ^ XnkY) . i

then (@ (X ^ y)) * J = @ (S ^ XnkY) by HILB10_2:def 1;

then eval (H,(@ (S ^ XnkY))) = eval (pA,(@ (X ^ y))) by A16, HILB10_2:25;

then X in A by A2, A45;

hence s in Y by A49, A45; :: thesis: verum

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

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
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 A2, A18;

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 A1, A9, AFINSQ_2:def 2;

x /^ nk is k -element by A21, A1, A9, AFINSQ_2:def 2;

then reconsider S = x /^ nk as k -element XFinSequence of NAT ;

A23: len (x | nk) = nk by CARD_1:def 7, A1;

reconsider XnkY = (x | nk) ^ y as nk + nA -element XFinSequence of NAT by A1;

A26: len (S ^ XnkY) = n + nA by A1, CARD_1:def 7;

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

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;( 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 A2, A18;

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 A1, A9, AFINSQ_2:def 2;

x /^ nk is k -element by A21, A1, A9, AFINSQ_2:def 2;

then reconsider S = x /^ nk as k -element XFinSequence of NAT ;

A23: len (x | nk) = nk by CARD_1:def 7, A1;

reconsider XnkY = (x | nk) ^ y as nk + nA -element XFinSequence of NAT by A1;

A26: len (S ^ XnkY) = n + nA by A1, CARD_1:def 7;

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

then
(@ (x ^ y)) * J = S ^ XnkY
by CARD_1:def 7, A1, A27, FUNCT_1:2;
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 A29, A26, A27, FUNCT_1:11, FUNCT_1:12;

end;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 A29, A26, A27, FUNCT_1:11, FUNCT_1:12;

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 A30, AFINSQ_1:20;

end;

( n in dom (I /^ n) & j = (len (((I | n) /^ nk) ^ (I | nk))) + n ) ) by A30, AFINSQ_1:20;

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;

end;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 A31, AFINSQ_1:20;

end;

( k in dom (I | nk) & j = (len ((I | n) /^ nk)) + k ) ) by A31, AFINSQ_1:20;

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 A9, A1, AFINSQ_2:def 2, AFINSQ_1:66, AFINSQ_1:def 3;

A35: nk + j in n by A1, A33, A9, AFINSQ_1:66, HILB10_3:3;

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 CARD_1:def 7, A1, A9;

Segm n = n ;

then nk + j < n + nA by NAT_1:44, A35, A7, XXREAL_0:2;

then nk + j in Segm (n + nA) by NAT_1:44;

then ((@ (x ^ y)) * J) . j = (@ (x ^ y)) . (nk + j) by FUNCT_1:17, A32, A30, A36, A34

.= (x ^ y) . (nk + j) by HILB10_2:def 1

.= (S ^ y) . j by A23, A37, A22, A33, A1, A9, A28, AFINSQ_1:def 3

.= S . j by A22, A33, A1, A9, AFINSQ_1:def 3

.= (S ^ XnkY) . j by A33, A38, AFINSQ_1:def 3 ;

hence ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum

end;A35: nk + j in n by A1, A33, A9, AFINSQ_1:66, HILB10_3:3;

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 CARD_1:def 7, A1, A9;

Segm n = n ;

then nk + j < n + nA by NAT_1:44, A35, A7, XXREAL_0:2;

then nk + j in Segm (n + nA) by NAT_1:44;

then ((@ (x ^ y)) * J) . j = (@ (x ^ y)) . (nk + j) by FUNCT_1:17, A32, A30, A36, A34

.= (x ^ y) . (nk + j) by HILB10_2:def 1

.= (S ^ y) . j by A23, A37, A22, A33, A1, A9, A28, AFINSQ_1:def 3

.= S . j by A22, A33, A1, A9, AFINSQ_1:def 3

.= (S ^ XnkY) . j by A33, A38, AFINSQ_1:def 3 ;

hence ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum

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

( 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 A39, A9, AFINSQ_1:66, AFINSQ_1:def 3, FUNCT_1:49;

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 A1, A39, A9, AFINSQ_1:66, XXREAL_0:2;

then A42: w in Segm (n + nA) by NAT_1:44;

J . j = w by A42, A40, A32, FUNCT_1:17;

then ((@ (x ^ y)) * J) . j = ((x | nk) ^ (S ^ y)) . w by A30, A28, HILB10_2:def 1

.= (x | nk) . w by AFINSQ_1:def 3, A39, A23, A9

.= ((x | nk) ^ y) . w by A39, A23, A9, AFINSQ_1:def 3

.= (S ^ XnkY) . j by A22, A39, A1, A9, A41, A23, AFINSQ_1:def 3 ;

hence ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum

end;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 A39, A9, AFINSQ_1:66, AFINSQ_1:def 3, FUNCT_1:49;

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 A1, A39, A9, AFINSQ_1:66, XXREAL_0:2;

then A42: w in Segm (n + nA) by NAT_1:44;

J . j = w by A42, A40, A32, FUNCT_1:17;

then ((@ (x ^ y)) * J) . j = ((x | nk) ^ (S ^ y)) . w by A30, A28, HILB10_2:def 1

.= (x | nk) . w by AFINSQ_1:def 3, A39, A23, A9

.= ((x | nk) ^ y) . w by A39, A23, A9, AFINSQ_1:def 3

.= (S ^ XnkY) . j by A22, A39, A1, A9, A41, A23, AFINSQ_1:def 3 ;

hence ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum

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

( 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 CARD_1:def 7, A1;

J . j = (I /^ n) . w by A43, AFINSQ_1:def 3

.= I . j by A9, A10, A43, AFINSQ_2:def 2

.= j by A29, A26, FUNCT_1:17 ;

then ((@ (x ^ y)) * J) . j = (x ^ y) . j by A30, HILB10_2:def 1

.= y . w by A9, A10, A43, A8, A21, AFINSQ_1:def 3

.= ((S ^ (x | nk)) ^ y) . j by A44, A9, A10, A43, A8, A21, AFINSQ_1:def 3

.= (S ^ XnkY) . j by AFINSQ_1:27 ;

hence ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum

end;A43: ( w in dom (I /^ n) & j = (len (((I | n) /^ nk) ^ (I | nk))) + w ) ;

A44: len (S ^ (x | nk)) = n by CARD_1:def 7, A1;

J . j = (I /^ n) . w by A43, AFINSQ_1:def 3

.= I . j by A9, A10, A43, AFINSQ_2:def 2

.= j by A29, A26, FUNCT_1:17 ;

then ((@ (x ^ y)) * J) . j = (x ^ y) . j by A30, HILB10_2:def 1

.= y . w by A9, A10, A43, A8, A21, AFINSQ_1:def 3

.= ((S ^ (x | nk)) ^ y) . j by A44, A9, A10, A43, A8, A21, AFINSQ_1:def 3

.= (S ^ XnkY) . j by AFINSQ_1:27 ;

hence ((@ (x ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum

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

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 NAT_1:11, CARD_1:def 7;

then A47: ( len (XnkY | nk) = nk & len (XnkY /^ nk) = (nk + nA) -' nk & (nk + nA) -' nk = (nk + nA) - nk ) by AFINSQ_1:54, AFINSQ_2:def 2;

reconsider y = XnkY /^ nk as nA -element XFinSequence of NAT by A47, CARD_1:def 7;

reconsider X = (XnkY | nk) ^ S as n -element XFinSequence of NAT by A1;

A48: X | nk = XnkY | nk by A47, AFINSQ_1:57;

(XnkY | nk) ^ S = (X | nk) ^ (X /^ nk) ;

then A49: X /^ nk = S by A48, AFINSQ_1:28;

A50: XnkY = (XnkY | nk) ^ y ;

A51: ( len X = n & len y = nA ) by CARD_1:def 7;

A52: len (X | nk) = nk by A47, AFINSQ_1:57;

A53: len (S ^ XnkY) = n + nA by CARD_1:def 7, A1;

A54: dom ((@ (X ^ y)) * J) = n + nA by FUNCT_2:def 1;

A55: X ^ y = (X | nk) ^ (S ^ y) by A48, AFINSQ_1:27;

for i being object st i in dom (S ^ XnkY) holds

((@ (X ^ y)) * J) . i = (S ^ XnkY) . i

proof

then
(@ (X ^ y)) * J = S ^ XnkY
by CARD_1:def 7, A1, A54, FUNCT_1:2;
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 A56, A53, A54, FUNCT_1:11, FUNCT_1:12;

end;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 A56, A53, A54, FUNCT_1:11, FUNCT_1:12;

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 A57, AFINSQ_1:20;

end;

( n in dom (I /^ n) & j = (len (((I | n) /^ nk) ^ (I | nk))) + n ) ) by A57, AFINSQ_1:20;

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;

end;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 A58, AFINSQ_1:20;

end;

( k in dom (I | nk) & j = (len ((I | n) /^ nk)) + k ) ) by A58, AFINSQ_1:20;

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 A9, A1, AFINSQ_2:def 2, AFINSQ_1:66, AFINSQ_1:def 3;

then A63: (I | n) . (nk + j) = I . (nk + j) by A1, HILB10_3:3, FUNCT_1:49;

A62: nk + j in n by A60, A1, HILB10_3:3, A9, AFINSQ_1:66;

A64: dom S c= dom (S ^ y) by AFINSQ_1:21;

A65: ( len S = k & k = len ((I | n) /^ nk) ) by CARD_1:def 7, A1, A9;

Segm n = n ;

then nk + j < n + nA by NAT_1:44, A62, A7, XXREAL_0:2;

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 A55, HILB10_2:def 1, A59, A57, A63, A61

.= (S ^ y) . j by A52, A64, A60, A1, A46, A9, AFINSQ_1:def 3

.= S . j by A60, A1, A46, A9, AFINSQ_1:def 3

.= (S ^ XnkY) . j by A60, A65, AFINSQ_1:def 3 ;

hence ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum

end;then A63: (I | n) . (nk + j) = I . (nk + j) by A1, HILB10_3:3, FUNCT_1:49;

A62: nk + j in n by A60, A1, HILB10_3:3, A9, AFINSQ_1:66;

A64: dom S c= dom (S ^ y) by AFINSQ_1:21;

A65: ( len S = k & k = len ((I | n) /^ nk) ) by CARD_1:def 7, A1, A9;

Segm n = n ;

then nk + j < n + nA by NAT_1:44, A62, A7, XXREAL_0:2;

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 A55, HILB10_2:def 1, A59, A57, A63, A61

.= (S ^ y) . j by A52, A64, A60, A1, A46, A9, AFINSQ_1:def 3

.= S . j by A60, A1, A46, A9, AFINSQ_1:def 3

.= (S ^ XnkY) . j by A60, A65, AFINSQ_1:def 3 ;

hence ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum

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

( 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 A66, A9, AFINSQ_1:66, AFINSQ_1:def 3, FUNCT_1:49;

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 A1, A66, A9, AFINSQ_1:66, XXREAL_0:2;

then A69: w in Segm (n + nA) by NAT_1:44;

J . j = w by A59, A69, FUNCT_1:17, A67;

then ((@ (X ^ y)) * J) . j = (X ^ y) . w by HILB10_2:def 1, A57

.= (X | nk) . w by AFINSQ_1:def 3, A66, A52, A9, A55

.= ((X | nk) ^ y) . w by A66, A52, A9, AFINSQ_1:def 3

.= (S ^ XnkY) . j by A48, A46, A1, A9, A68, A47, A66, AFINSQ_1:def 3 ;

hence ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum

end;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 A66, A9, AFINSQ_1:66, AFINSQ_1:def 3, FUNCT_1:49;

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 A1, A66, A9, AFINSQ_1:66, XXREAL_0:2;

then A69: w in Segm (n + nA) by NAT_1:44;

J . j = w by A59, A69, FUNCT_1:17, A67;

then ((@ (X ^ y)) * J) . j = (X ^ y) . w by HILB10_2:def 1, A57

.= (X | nk) . w by AFINSQ_1:def 3, A66, A52, A9, A55

.= ((X | nk) ^ y) . w by A66, A52, A9, AFINSQ_1:def 3

.= (S ^ XnkY) . j by A48, A46, A1, A9, A68, A47, A66, AFINSQ_1:def 3 ;

hence ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum

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

( 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 A1, CARD_1:def 7;

J . j = (I /^ n) . w by A70, AFINSQ_1:def 3

.= I . j by A9, A10, A70, AFINSQ_2:def 2

.= j by A56, A53, FUNCT_1:17 ;

then ((@ (X ^ y)) * J) . j = (X ^ y) . j by HILB10_2:def 1, A57

.= y . w by A9, A10, A70, A8, A51, AFINSQ_1:def 3

.= ((S ^ (X | nk)) ^ y) . j by A71, A9, A10, A70, A8, A51, AFINSQ_1:def 3

.= (S ^ XnkY) . j by AFINSQ_1:27, A48, A50 ;

hence ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum

end;A70: ( w in dom (I /^ n) & j = (len (((I | n) /^ nk) ^ (I | nk))) + w ) ;

A71: len (S ^ (X | nk)) = n by A1, CARD_1:def 7;

J . j = (I /^ n) . w by A70, AFINSQ_1:def 3

.= I . j by A9, A10, A70, AFINSQ_2:def 2

.= j by A56, A53, FUNCT_1:17 ;

then ((@ (X ^ y)) * J) . j = (X ^ y) . j by HILB10_2:def 1, A57

.= y . w by A9, A10, A70, A8, A51, AFINSQ_1:def 3

.= ((S ^ (X | nk)) ^ y) . j by A71, A9, A10, A70, A8, A51, AFINSQ_1:def 3

.= (S ^ XnkY) . j by AFINSQ_1:27, A48, A50 ;

hence ((@ (X ^ y)) * J) . j = (S ^ XnkY) . j ; :: thesis: verum

then (@ (X ^ y)) * J = @ (S ^ XnkY) by HILB10_2:def 1;

then eval (H,(@ (S ^ XnkY))) = eval (pA,(@ (X ^ y))) by A16, HILB10_2:25;

then X in A by A2, A45;

hence s in Y by A49, A45; :: thesis: verum