deffunc H1( Nat, Nat, Nat) -> Element of omega = $1 ! ;
A1:
for n being Nat
for i1, i2, i3, i4 being Element of n holds { p where p is b1 -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of (n -xtuples_of NAT)
by Th32;
defpred S1[ Nat, Nat, natural object , Nat, Nat, Nat] means ( $1 = Product (1 + ($3 * (idseq $2))) & $3 >= 1 );
A2:
for n being Nat
for i1, i2, i3, i4, i5, i6 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S1[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT)
by Th35;
A3:
for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S1[p . i1,p . i2,H1(p . i3,p . i4,p . i5),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 4(A2, A1);
deffunc H2( Nat, Nat, Nat) -> Element of omega = (1 * $1) + 1;
A4:
for n being Nat
for i1, i2, i3, i4 being Element of n holds { p where p is b1 -element XFinSequence of NAT : H2(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:15;
defpred S2[ Nat, Nat, natural object , Nat, Nat, Nat] means ( $1 = Product (1 + (($2 !) * (idseq $3))) & $2 ! >= 1 );
A5:
for n being Nat
for i1, i3, i2, i4, i5, i6 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S2[p . i1,p . i3,p . i2,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT)
by A3;
A6:
for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S2[p . i1,p . i2,H2(p . i3,p . i4,p . i5),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 4(A5, A4);
let n be Nat; for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i3 = Product (1 + (((p . i1) !) * (idseq (1 + (p . i2))))) } is diophantine Subset of (n -xtuples_of NAT)
let i1, i2, i3 be Element of n; { p where p is n -element XFinSequence of NAT : p . i3 = Product (1 + (((p . i1) !) * (idseq (1 + (p . i2))))) } is diophantine Subset of (n -xtuples_of NAT)
defpred S3[ XFinSequence of NAT ] means S2[$1 . i3,$1 . i1,(1 * ($1 . i2)) + 1,1 * ($1 . i3),$1 . i3,$1 . i3];
defpred S4[ XFinSequence of NAT ] means $1 . i3 = Product (1 + ((($1 . i1) !) * (idseq (1 + ($1 . i2)))));
A7:
for p being n -element XFinSequence of NAT holds
( S3[p] iff S4[p] )
by NAT_1:14;
{ p where p is n -element XFinSequence of NAT : S3[p] } = { q where q is n -element XFinSequence of NAT : S4[q] }
from HILB10_3:sch 2(A7);
hence
{ p where p is n -element XFinSequence of NAT : p . i3 = Product (1 + (((p . i1) !) * (idseq (1 + (p . i2))))) } is diophantine Subset of (n -xtuples_of NAT)
by A6; verum