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

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

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

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

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

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

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 ;
reconsider nk = n - (k + 1) as Nat by ;
set f = <%i2%> ^ Idk;
A4: rng <%i2%> = {i2} by AFINSQ_1:33;
{i2} misses k by ;
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 ;
then A9: Segm k c= Segm n by NAT_1:39;
i2 in n by ;
then {i2} c= n by ZFMISC_1:31;
then k \/ {i2} c= n by ;
then A10: rng (<%i2%> ^ Idk) c= n by ;
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 ;
A12: Segm (k + 1) c= Segm n by ;
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 ;
A14: ( rng (<%i2%> ^ Idk) misses rng g & dom (<%i2%> ^ Idk) misses dom g ) by ;
then A15: (<%i2%> ^ Idk) +* g is one-to-one by ;
A16: dom ((<%i2%> ^ Idk) +* g) = (k + 1) \/ (n \ (k + 1)) by
.= (k + 1) \/ n by XBOOLE_1:39
.= n by ;
A17: rng ((<%i2%> ^ Idk) +* g) = (rng (<%i2%> ^ Idk)) \/ (rng g) by
.= n \/ (rng (<%i2%> ^ Idk)) by
.= n by ;
then reconsider fg = (<%i2%> ^ Idk) +* g as Function of n,n by ;
card n = card n ;
then fg is onto by ;
then reconsider fg = fg as Permutation of n by A15;
defpred S1[ 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 S2[ 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
( S1[p] iff S2[p] )
proof
let p be n -element XFinSequence of NAT ; :: thesis: ( S1[p] iff S2[p] )
A19: len p = n by CARD_1:def 7;
then dom (p * fg) = n by ;
then reconsider pfg = p * fg as XFinSequence by AFINSQ_1:5;
set I = <%(p . i2)%>;
len pfg = n by ;
then A20: len (pfg | (k + 1)) = k + 1 by ;
A21: ( len (p | k) = k & len <%(p . i2)%> = 1 ) by ;
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: ( 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 ;
then A25: ( pfg . i = p . (fg . i) & not i in dom g ) by ;
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 ;
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 ;
then ( i = 0 & i in dom <%i2%> ) by ;
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 ; :: thesis: verum
end;
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
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 ;
j in dom Idk by ;
then ( (<%i2%> ^ Idk) . i = Idk . j & Idk . j = j ) by ;
hence (<%(p . i2)%> ^ (p | k)) . i = (pfg | (k + 1)) . i by ; :: thesis: verum
end;
end;
end;
hence ( S1[p] iff S2[p] ) by A20, A22, AFINSQ_1:8; :: thesis: verum
end;
{ p where p is n -element XFinSequence of NAT : S1[p] } = { q where q is n -element XFinSequence of NAT : S2[q] } from 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 () by ; :: thesis: verum