let k be Nat; :: thesis:
let P be INT -valued Polynomial of (k + 1),F_Real; :: thesis:
let a be Integer; :: thesis:
let n be Nat; :: thesis:
let i1, i2 be Element of n; :: thesis:
assume A1: ( k + 1 <= n & k in i2 ) ; :: thesis:
set k1 = k + 1;
dom (id k) = k ;
then reconsider Idk = id k as XFinSequence by AFINSQ_1:5;
A2: len Idk = k ;
A3: rng (id k) = Segm k ;
then reconsider Idk = Idk as k -element XFinSequence of NAT by A2, CARD_1:def 7;
reconsider nk = n - (k + 1) as Nat by A1, NAT_1:21;
set f = <%i2%> ^ Idk;
A4: rng <%i2%> = {i2} by AFINSQ_1:33;
{i2} misses k by A1, ZFMISC_1:50;
then rng <%i2%> misses rng Idk by AFINSQ_1:33;
then A6: <%i2%> ^ Idk is one-to-one by CARD_FIN:52;
set R = rng (<%i2%> ^ Idk);
A7: len (<%i2%> ^ Idk) = k + 1 by CARD_1:def 7;
A8: card (dom (<%i2%> ^ Idk)) = k + 1 by CARD_1:def 7;
A: k < n by A1, NAT_1:13;
then A9: Segm k c= Segm n by NAT_1:39;
i2 in n by A1, SUBSET_1:def 1;
then {i2} c= n by ZFMISC_1:31;
then k \/ {i2} c= n by A9, XBOOLE_1:8;
then A10: rng (<%i2%> ^ Idk) c= n by AFINSQ_1:26, A4, A3;
then card (n \ (rng (<%i2%> ^ Idk))) = (card n) - (card (rng (<%i2%> ^ Idk))) by CARD_2:44;
then A11: card (n \ (rng (<%i2%> ^ Idk))) = nk by A8, A6, CARD_1:70;
A12: Segm (k + 1) c= Segm n by A1, NAT_1:39;
then card (n \ (k + 1)) = (card n) - (card (k + 1)) by CARD_2:44
.= nk ;
then consider g being Function such that
A13: ( g is one-to-one & dom g = n \ (k + 1) & rng g = n \ (rng (<%i2%> ^ Idk)) ) by A11, CARD_1:5, WELLORD2:def 4;
A14: ( rng (<%i2%> ^ Idk) misses rng g & dom (<%i2%> ^ Idk) misses dom g ) by A7, A13, XBOOLE_1:79;
then A15: (<%i2%> ^ Idk) +* g is one-to-one by A6, A13, FUNCT_4:92;
A16: dom ((<%i2%> ^ Idk) +* g) = (k + 1) \/ (n \ (k + 1)) by A7, A13, FUNCT_4:def 1
.= (k + 1) \/ n by XBOOLE_1:39
.= n by A12, XBOOLE_1:12 ;
A17: rng ((<%i2%> ^ Idk) +* g) = (rng (<%i2%> ^ Idk)) \/ (rng g) by A14, NECKLACE:6
.= n \/ (rng (<%i2%> ^ Idk)) by A13, XBOOLE_1:39
.= n by A10, XBOOLE_1:12 ;
then reconsider fg = (<%i2%> ^ Idk) +* g as Function of n,n by A16, FUNCT_2:2;
card n = card n ;
then fg is onto by A15, FINSEQ_4:63;
then reconsider fg = fg as Permutation of n by A15;
defpred S₁[ XFinSequence of NAT ] means for q being k + 1 -element XFinSequence of NAT st q = ($1 * fg) | (k + 1) holds
a * ($1 . i1) = eval (P,(@ q));
defpred S₂[ XFinSequence of NAT ] means for q being k + 1 -element XFinSequence of NAT st q = <%($1 . i2)%> ^ ($1 | k) holds
a * ($1 . i1) = eval (P,(@ q));
A18: for p being n -element XFinSequence of NAT holds
( S₁[p] iff S₂[p] )

proof

let p be n -element XFinSequence of NAT ; :: thesis:
A19: len p = n by CARD_1:def 7;
then dom (p * fg) = n by A17, A16, RELAT_1:27;
then reconsider pfg = p * fg as XFinSequence by AFINSQ_1:5;
set I = <%(p . i2)%>;
len pfg = n by A19, A17, A16, RELAT_1:27;
then A20: len (pfg | (k + 1)) = k + 1 by A1, AFINSQ_1:54;
A21: ( len (p | k) = k & len <%(p . i2)%> = 1 ) by AFINSQ_1:11, A, A19, CARD_1:def 7;
then A22: len (<%(p . i2)%> ^ (p | k)) = k + 1 by AFINSQ_1:17;
for i being Nat st i in dom (<%(p . i2)%> ^ (p | k)) holds
(<%(p . i2)%> ^ (p | k)) . i = (pfg | (k + 1)) . i

proof

let i be Nat; :: thesis:
assume A23: i in dom (<%(p . i2)%> ^ (p | k)) ; :: thesis:
then A24: ( i in dom pfg & i in k + 1 & (pfg | (k + 1)) . i = pfg . i ) by RELAT_1:57, FUNCT_1:47, A20, A22;
then A25: ( pfg . i = p . (fg . i) & not i in dom g ) by FUNCT_1:12, A13, XBOOLE_1:79, XBOOLE_0:3;
then A26: fg . i = (<%i2%> ^ Idk) . i by FUNCT_4:11;
A27: len <%i2%> = 1 by CARD_1:def 7;

per cases by A23, AFINSQ_1:20;

suppose A28: i in dom <%(p . i2)%> ; :: thesis:

then ( i < len <%(p . i2)%> & len <%(p . i2)%> = 1 ) by AFINSQ_1:66, CARD_1:def 7;
then ( i = 0 & i in dom <%i2%> ) by CARD_1:def 7, A28, NAT_1:14;
then ( (<%i2%> ^ Idk) . i = <%i2%> . i & <%i2%> . i = i2 & <%(p . i2)%> . i = p . i2 ) by AFINSQ_1:def 3;
hence (<%(p . i2)%> ^ (p | k)) . i = (pfg | (k + 1)) . i by A24, A25, A26, A28, AFINSQ_1:def 3; :: thesis:

end;

suppose ex j being Nat st
( j in dom (p | k) & i = (len <%(p . i2)%>) + j ) ; :: thesis:

then consider j being Nat such that
A29: ( j in dom (p | k) & i = (len <%(p . i2)%>) + j ) ;
A30: ( (<%(p . i2)%> ^ (p | k)) . i = (p | k) . j & (p | k) . j = p . j ) by A29, AFINSQ_1:def 3, FUNCT_1:47;
j in dom Idk by A, A19, A29, AFINSQ_1:11;
then ( (<%i2%> ^ Idk) . i = Idk . j & Idk . j = j ) by A21, A27, A29, AFINSQ_1:def 3, FUNCT_1:17;
hence (<%(p . i2)%> ^ (p | k)) . i = (pfg | (k + 1)) . i by A30, A24, A25, FUNCT_4:11; :: thesis:

end;

hence ( S₁[p] iff S₂[p] ) by A20, A22, AFINSQ_1:8; :: thesis:

end;

{ p where p is n -element XFinSequence of NAT : S₁[p] } = { q where q is n -element XFinSequence of NAT : S₂[q] } from HILB10_3:sch 2(A18);
hence { p where p is n -element XFinSequence of NAT : for q being k + 1 -element XFinSequence of NAT st q = <%(p . i2)%> ^ (p | k) holds
a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT) by Th13, A1; :: thesis: