let n be Nat; for i1, i2, i3 being Element of n st n <> 0 holds
{ p where p is n -element XFinSequence of NAT : ( p . i3 = Product (1 + ((p . i1) * (idseq (p . i2)))) & p . i1 >= 1 ) } is diophantine Subset of (n -xtuples_of NAT)
let i1, i2, i3 be Element of n; ( n <> 0 implies { p where p is n -element XFinSequence of NAT : ( p . i3 = Product (1 + ((p . i1) * (idseq (p . i2)))) & p . i1 >= 1 ) } is diophantine Subset of (n -xtuples_of NAT) )
set n12 = n + 13;
defpred S1[ XFinSequence of NAT ] means ( $1 . i3 = Product (1 + (($1 . i1) * (idseq ($1 . i2)))) & $1 . i1 >= 1 );
set RR = { p where p is n -element XFinSequence of NAT : S1[p] } ;
assume A1:
n <> 0
; { p where p is n -element XFinSequence of NAT : ( p . i3 = Product (1 + ((p . i1) * (idseq (p . i2)))) & p . i1 >= 1 ) } is diophantine Subset of (n -xtuples_of NAT)
n = n + 0
;
then reconsider X1 = i1, X = i2, Y = i3, U = n, W = n + 1, Y1 = n + 2, Y2 = n + 3, Y3 = n + 4, Y4 = n + 5, Y5 = n + 6, X1W = n + 7, WX = n + 8, Y1Y2 = n + 9, Y1Y2Y3 = n + 10, X1X = n + 11, ONE = n + 12 as Element of n + 13 by HILB10_3:2, HILB10_3:3;
defpred S2[ XFinSequence of NAT ] means 1 * ($1 . X1) >= (0 * ($1 . Y)) + 1;
A2:
{ p where p is n + 13 -element XFinSequence of NAT : S2[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
by HILB10_3:8;
defpred S3[ XFinSequence of NAT ] means 1 * ($1 . U) > (1 * ($1 . Y)) + 0;
A3:
{ p where p is n + 13 -element XFinSequence of NAT : S3[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
by HILB10_3:7;
defpred S4[ XFinSequence of NAT ] means 1 * ($1 . X1W) = (1 * ($1 . X1)) * ($1 . W);
A4:
{ p where p is n + 13 -element XFinSequence of NAT : S4[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
by HILB10_3:9;
defpred S5[ XFinSequence of NAT ] means $1 . ONE = 1;
A5:
{ p where p is n + 13 -element XFinSequence of NAT : S5[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
by HILB10_3:14;
defpred S6[ XFinSequence of NAT ] means 1 * ($1 . X1W),1 * ($1 . ONE) are_congruent_mod 1 * ($1 . U);
A6:
{ p where p is n + 13 -element XFinSequence of NAT : S6[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
by HILB10_3:21;
defpred S7[ XFinSequence of NAT ] means $1 . Y1 = ($1 . X1) |^ ($1 . X);
A7:
{ p where p is n + 13 -element XFinSequence of NAT : S7[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
by HILB10_3:24;
defpred S8[ XFinSequence of NAT ] means $1 . Y2 = ($1 . X) ! ;
A8:
{ p where p is n + 13 -element XFinSequence of NAT : S8[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
by Th32;
defpred S9[ XFinSequence of NAT ] means 1 * ($1 . WX) = ((1 * ($1 . W)) + (1 * ($1 . X))) + 0;
A9:
{ p where p is n + 13 -element XFinSequence of NAT : S9[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
by HILB10_3:11;
defpred S10[ XFinSequence of NAT ] means ( $1 . WX >= $1 . X & $1 . Y3 = ($1 . WX) choose ($1 . X) );
A10:
{ p where p is n + 13 -element XFinSequence of NAT : S10[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
by Th30;
defpred S11[ XFinSequence of NAT ] means 1 * ($1 . Y1Y2) = (1 * ($1 . Y1)) * ($1 . Y2);
A11:
{ p where p is n + 13 -element XFinSequence of NAT : S11[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
by HILB10_3:9;
defpred S12[ XFinSequence of NAT ] means 1 * ($1 . Y1Y2Y3) = (1 * ($1 . Y1Y2)) * ($1 . Y3);
A12:
{ p where p is n + 13 -element XFinSequence of NAT : S12[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
by HILB10_3:9;
defpred S13[ XFinSequence of NAT ] means 1 * ($1 . Y1Y2Y3),1 * ($1 . Y) are_congruent_mod 1 * ($1 . U);
A13:
{ p where p is n + 13 -element XFinSequence of NAT : S13[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
by HILB10_3:21;
defpred S14[ XFinSequence of NAT ] means 1 * ($1 . X1X) = (1 * ($1 . X1)) * ($1 . X);
A14:
{ p where p is n + 13 -element XFinSequence of NAT : S14[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
by HILB10_3:9;
defpred S15[ XFinSequence of NAT ] means 1 * ($1 . Y4) = (1 * ($1 . X1X)) + 1;
A15:
{ p where p is n + 13 -element XFinSequence of NAT : S15[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
by HILB10_3:6;
defpred S16[ XFinSequence of NAT ] means $1 . Y5 = ($1 . Y4) |^ ($1 . X);
A16:
{ p where p is n + 13 -element XFinSequence of NAT : S16[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
by HILB10_3:24;
defpred S17[ XFinSequence of NAT ] means 1 * ($1 . U) > (1 * ($1 . Y5)) + 0;
A17:
{ p where p is n + 13 -element XFinSequence of NAT : S17[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
by HILB10_3:7;
defpred S18[ XFinSequence of NAT ] means ( S2[$1] & S3[$1] );
A18:
{ p where p is n + 13 -element XFinSequence of NAT : S18[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
from HILB10_3:sch 3(A2, A3);
defpred S19[ XFinSequence of NAT ] means ( S18[$1] & S4[$1] );
A19:
{ p where p is n + 13 -element XFinSequence of NAT : S19[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
from HILB10_3:sch 3(A18, A4);
defpred S20[ XFinSequence of NAT ] means ( S19[$1] & S5[$1] );
A20:
{ p where p is n + 13 -element XFinSequence of NAT : S20[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
from HILB10_3:sch 3(A19, A5);
defpred S21[ XFinSequence of NAT ] means ( S20[$1] & S6[$1] );
A21:
{ p where p is n + 13 -element XFinSequence of NAT : S21[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
from HILB10_3:sch 3(A20, A6);
defpred S22[ XFinSequence of NAT ] means ( S21[$1] & S7[$1] );
A22:
{ p where p is n + 13 -element XFinSequence of NAT : S22[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
from HILB10_3:sch 3(A21, A7);
defpred S23[ XFinSequence of NAT ] means ( S22[$1] & S8[$1] );
A23:
{ p where p is n + 13 -element XFinSequence of NAT : S23[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
from HILB10_3:sch 3(A22, A8);
defpred S24[ XFinSequence of NAT ] means ( S23[$1] & S9[$1] );
A24:
{ p where p is n + 13 -element XFinSequence of NAT : S24[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
from HILB10_3:sch 3(A23, A9);
defpred S25[ XFinSequence of NAT ] means ( S24[$1] & S10[$1] );
A25:
{ p where p is n + 13 -element XFinSequence of NAT : S25[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
from HILB10_3:sch 3(A24, A10);
defpred S26[ XFinSequence of NAT ] means ( S25[$1] & S11[$1] );
A26:
{ p where p is n + 13 -element XFinSequence of NAT : S26[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
from HILB10_3:sch 3(A25, A11);
defpred S27[ XFinSequence of NAT ] means ( S26[$1] & S12[$1] );
A27:
{ p where p is n + 13 -element XFinSequence of NAT : S27[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
from HILB10_3:sch 3(A26, A12);
defpred S28[ XFinSequence of NAT ] means ( S27[$1] & S13[$1] );
A28:
{ p where p is n + 13 -element XFinSequence of NAT : S28[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
from HILB10_3:sch 3(A27, A13);
defpred S29[ XFinSequence of NAT ] means ( S28[$1] & S14[$1] );
A29:
{ p where p is n + 13 -element XFinSequence of NAT : S29[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
from HILB10_3:sch 3(A28, A14);
defpred S30[ XFinSequence of NAT ] means ( S29[$1] & S15[$1] );
A30:
{ p where p is n + 13 -element XFinSequence of NAT : S30[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
from HILB10_3:sch 3(A29, A15);
defpred S31[ XFinSequence of NAT ] means ( S30[$1] & S16[$1] );
A31:
{ p where p is n + 13 -element XFinSequence of NAT : S31[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
from HILB10_3:sch 3(A30, A16);
defpred S32[ XFinSequence of NAT ] means ( S31[$1] & S17[$1] );
set PP = { p where p is n + 13 -element XFinSequence of NAT : S32[p] } ;
A32:
{ p where p is n + 13 -element XFinSequence of NAT : S32[p] } is diophantine Subset of ((n + 13) -xtuples_of NAT)
from HILB10_3:sch 3(A31, A17);
reconsider PPn = { (p | n) where p is n + 13 -element XFinSequence of NAT : p in { p where p is n + 13 -element XFinSequence of NAT : S32[p] } } as diophantine Subset of (n -xtuples_of NAT) by NAT_1:11, HILB10_3:5, A32;
A33:
PPn c= { p where p is n -element XFinSequence of NAT : S1[p] }
{ p where p is n -element XFinSequence of NAT : S1[p] } c= PPn
proof
let x be
object ;
TARSKI:def 3 ( not x in { p where p is n -element XFinSequence of NAT : S1[p] } or x in PPn )
assume
x in { p where p is n -element XFinSequence of NAT : S1[p] }
;
x in PPn
then consider p being
n -element XFinSequence of
NAT such that A36:
(
x = p &
S1[
p] )
;
consider u,
w,
y1,
y2,
y3,
y4,
y5 being
Nat such that A37:
(
u > p . i3 &
(p . i1) * w,1
are_congruent_mod u &
y1 = (p . i1) |^ (p . i2) &
y2 = (p . i2) ! &
y3 = (w + (p . i2)) choose (p . i2) &
(y1 * y2) * y3,
p . i3 are_congruent_mod u &
y4 = 1
+ ((p . i1) * (p . i2)) &
y5 = y4 |^ (p . i2) &
u > y5 )
by A36, Th20;
reconsider u =
u,
w =
w,
n =
n,
y1 =
y1,
y2 =
y2,
y3 =
y3,
y4 =
y4,
y5 =
y5 as
Element of
NAT by ORDINAL1:def 12;
reconsider x1w =
(p . i1) * w,
wx =
w + (p . i2),
y12 =
y1 * y2,
y123 =
(y1 * y2) * y3,
x1x =
(p . i1) * (p . i2),
One = 1 as
Element of
NAT ;
set Y1 =
(((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>;
set Y2 =
((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>;
set Y =
((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>);
set PY =
p ^ (((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>));
reconsider PY =
p ^ (((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) as
XFinSequence of
NAT ;
A38:
(
len p = n &
len (((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) = 13 &
len ((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) = 9 &
len (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>) = 4 )
by CARD_1:def 7;
A39:
PY | n = p
by A38, AFINSQ_1:57;
A40:
PY . i2 =
(PY | n) . i2
by A1, HILB10_3:4
.=
p . i2
by A38, AFINSQ_1:57
;
0 in dom (((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>))
by AFINSQ_1:66;
then A41:
PY . (n + 0) =
(((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) . 0
by A38, AFINSQ_1:def 3
.=
((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) . 0
by A38, AFINSQ_1:51
.=
u
by AFINSQ_1:50
;
1
in dom (((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>))
by A38, AFINSQ_1:66;
then A42:
PY . (n + 1) =
(((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) . 1
by A38, AFINSQ_1:def 3
.=
((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) . 1
by A38, AFINSQ_1:51
.=
w
by AFINSQ_1:50
;
2
in dom (((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>))
by A38, AFINSQ_1:66;
then A43:
PY . (n + 2) =
(((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) . 2
by A38, AFINSQ_1:def 3
.=
((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) . 2
by A38, AFINSQ_1:51
.=
y1
by AFINSQ_1:50
;
3
in dom (((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>))
by A38, AFINSQ_1:66;
then A44:
PY . (n + 3) =
(((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) . 3
by A38, AFINSQ_1:def 3
.=
((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) . 3
by A38, AFINSQ_1:51
.=
y2
by AFINSQ_1:50
;
4
in dom (((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>))
by A38, AFINSQ_1:66;
then A45:
PY . (n + 4) =
(((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) . 4
by A38, AFINSQ_1:def 3
.=
((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) . 4
by A38, AFINSQ_1:51
.=
y3
by AFINSQ_1:50
;
5
in dom (((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>))
by A38, AFINSQ_1:66;
then A46:
PY . (n + 5) =
(((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) . 5
by A38, AFINSQ_1:def 3
.=
((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) . 5
by A38, AFINSQ_1:51
.=
y4
by AFINSQ_1:50
;
6
in dom (((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>))
by A38, AFINSQ_1:66;
then A47:
PY . (n + 6) =
(((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) . 6
by A38, AFINSQ_1:def 3
.=
((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) . 6
by A38, AFINSQ_1:51
.=
y5
by AFINSQ_1:50
;
7
in dom (((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>))
by A38, AFINSQ_1:66;
then A48:
PY . (n + 7) =
(((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) . 7
by A38, AFINSQ_1:def 3
.=
((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) . 7
by A38, AFINSQ_1:51
.=
x1w
by AFINSQ_1:50
;
8
in dom (((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>))
by A38, AFINSQ_1:66;
then A49:
PY . (n + 8) =
(((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) . 8
by A38, AFINSQ_1:def 3
.=
((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) . 8
by A38, AFINSQ_1:51
.=
wx
by AFINSQ_1:50
;
A50:
( 9
in dom (((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) &
0 in dom (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>) )
by A38, AFINSQ_1:66;
then A51:
PY . (n + 9) =
(((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) . (9 + 0)
by A38, AFINSQ_1:def 3
.=
(((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>) . 0
by A38, A50, AFINSQ_1:def 3
.=
y12
by AFINSQ_1:45
;
A52:
( 10
in dom (((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) & 1
in dom (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>) )
by A38, AFINSQ_1:66;
then A53:
PY . (n + 10) =
(((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) . (9 + 1)
by A38, AFINSQ_1:def 3
.=
(((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>) . 1
by A38, A52, AFINSQ_1:def 3
.=
y123
by AFINSQ_1:45
;
A54:
( 11
in dom (((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) & 2
in dom (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>) )
by A38, AFINSQ_1:66;
then A55:
PY . (n + 11) =
(((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) . (9 + 2)
by A38, AFINSQ_1:def 3
.=
(((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>) . 2
by A38, A54, AFINSQ_1:def 3
.=
x1x
by AFINSQ_1:45
;
A56:
( 12
in dom (((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) & 3
in dom (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>) )
by A38, AFINSQ_1:66;
then A57:
PY . (n + 12) =
(((((((((<%u%> ^ <%w%>) ^ <%y1%>) ^ <%y2%>) ^ <%y3%>) ^ <%y4%>) ^ <%y5%>) ^ <%x1w%>) ^ <%wx%>) ^ (((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>)) . (9 + 3)
by A38, AFINSQ_1:def 3
.=
(((<%y12%> ^ <%y123%>) ^ <%x1x%>) ^ <%One%>) . 3
by A38, A56, AFINSQ_1:def 3
.=
One
by AFINSQ_1:45
;
S32[
PY]
by A36, A37, A39, A1, HILB10_3:4, A40, A41, A42, A43, A44, A45, A46, A47, A48, A49, A51, A53, A55, A57, NAT_1:11;
then
PY in { p where p is n + 13 -element XFinSequence of NAT : S32[p] }
;
hence
x in PPn
by A39, A36;
verum
end;
hence
{ p where p is n -element XFinSequence of NAT : ( p . i3 = Product (1 + ((p . i1) * (idseq (p . i2)))) & p . i1 >= 1 ) } is diophantine Subset of (n -xtuples_of NAT)
by A33, XBOOLE_0:def 10; verum