let k be Nat; :: thesis: for P being INT -valued Polynomial of (k + 1),F_Real

for a being Integer

for n being Nat

for i1, i2 being Element of n st k + 1 <= n & k in i2 holds

{ p where p is b_{3} -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)

let P be INT -valued Polynomial of (k + 1),F_Real; :: thesis: for a being Integer

for n being Nat

for i1, i2 being Element of n st k + 1 <= n & k in i2 holds

{ p where p is b_{2} -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)

let a be Integer; :: thesis: for n being Nat

for i1, i2 being Element of n st k + 1 <= n & k in i2 holds

{ p where p is b_{1} -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)

let n be Nat; :: thesis: for i1, i2 being Element of n st k + 1 <= n & k in i2 holds

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

let i1, i2 be Element of n; :: thesis: ( k + 1 <= n & k in i2 implies { 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) )

assume A1: ( k + 1 <= n & k in i2 ) ; :: thesis: { 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)

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_{1}[ 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_{2}[ 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_{1}[p] iff S_{2}[p] )
_{1}[p] } = { q where q is n -element XFinSequence of NAT : S_{2}[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: verum

for a being Integer

for n being Nat

for i1, i2 being Element of n st k + 1 <= n & k in i2 holds

{ p where p is b

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

let P be INT -valued Polynomial of (k + 1),F_Real; :: thesis: for a being Integer

for n being Nat

for i1, i2 being Element of n st k + 1 <= n & k in i2 holds

{ p where p is b

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

let a be Integer; :: thesis: for n being Nat

for i1, i2 being Element of n st k + 1 <= n & k in i2 holds

{ p where p is b

a * (p . i1) = eval (P,(@ q)) } is diophantine Subset of (n -xtuples_of NAT)

let n be Nat; :: thesis: for i1, i2 being Element of n st k + 1 <= n & k in i2 holds

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

let i1, i2 be Element of n; :: thesis: ( k + 1 <= n & k in i2 implies { 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) )

assume A1: ( k + 1 <= n & k in i2 ) ; :: thesis: { 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)

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

a * ($1 . i1) = eval (P,(@ q));

defpred S

a * ($1 . i1) = eval (P,(@ q));

A18: for p being n -element XFinSequence of NAT holds

( S

proof

{ p where p is n -element XFinSequence of NAT : S
let p be n -element XFinSequence of NAT ; :: thesis: ( S_{1}[p] iff S_{2}[p] )

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_{1}[p] iff S_{2}[p] )
by A20, A22, AFINSQ_1:8; :: thesis: verum

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

hence
( S
let i be Nat; :: thesis: ( i in dom (<%(p . i2)%> ^ (p | k)) implies (<%(p . i2)%> ^ (p | k)) . i = (pfg | (k + 1)) . i )

assume A23: i in dom (<%(p . i2)%> ^ (p | k)) ; :: thesis: (<%(p . i2)%> ^ (p | k)) . i = (pfg | (k + 1)) . i

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;

end;assume A23: i in dom (<%(p . i2)%> ^ (p | k)) ; :: thesis: (<%(p . i2)%> ^ (p | k)) . i = (pfg | (k + 1)) . i

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
( i in dom <%(p . i2)%> or ex j being Nat st

( j in dom (p | k) & i = (len <%(p . i2)%>) + j ) ) by A23, AFINSQ_1:20;

end;

( j in dom (p | k) & i = (len <%(p . i2)%>) + j ) ) by A23, AFINSQ_1:20;

suppose A28:
i in dom <%(p . i2)%>
; :: thesis: (<%(p . i2)%> ^ (p | k)) . i = (pfg | (k + 1)) . i

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: verum

end;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: verum

suppose
ex j being Nat st

( j in dom (p | k) & i = (len <%(p . i2)%>) + j ) ; :: thesis: (<%(p . i2)%> ^ (p | k)) . i = (pfg | (k + 1)) . i

( j in dom (p | k) & i = (len <%(p . i2)%>) + j ) ; :: thesis: (<%(p . i2)%> ^ (p | k)) . i = (pfg | (k + 1)) . i

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: verum

end;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: verum

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: verum