deffunc H1( Nat, Nat, Nat) -> set = (1 * $1) + (- 1);
A1:
for n being Nat
for i1, i2, i3, i4 being Element of n
for a being Integer holds { p where p is b1 -element XFinSequence of NAT : H1(p . i1,p . i2,p . i3) = a * (p . i4) } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:6;
defpred S1[ Nat, Nat, Integer] means (1 * $1) * $2 = $3;
A2:
for n being Nat
for i1, i2, i3 being Element of n
for a being Integer holds { p where p is b1 -element XFinSequence of NAT : S1[p . i1,p . i2,a * (p . i3)] } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:9;
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)] } is diophantine Subset of (n -xtuples_of NAT)
from HILB10_3:sch 5(A2, A1);
deffunc H2( Nat, Nat, Nat) -> Element of omega = $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 Th32;
defpred S2[ Nat, Nat, natural object , Nat, Nat, Nat] means (1 * $1) * $3 = (1 * $2) - 1;
A5:
now 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)let n be
Nat;
for i1, i3, i2, i4, i5, i6 being Element of n holds { p where p is n -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)let i1,
i3,
i2,
i4,
i5,
i6 be
Element of
n;
{ p where p is n -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)defpred S3[
XFinSequence of
NAT ]
means S1[$1
. i1,$1
. i2,
(1 * ($1 . i3)) + (- 1)];
defpred S4[
XFinSequence of
NAT ]
means S2[$1
. i1,$1
. i3,$1
. i2,$1
. i4,$1
. i5,$1
. i6];
A6:
for
p being
n -element XFinSequence of
NAT holds
(
S3[
p] iff
S4[
p] )
;
{ 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(A6);
hence
{ p where p is n -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;
verum end;
A7:
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);
defpred S3[ Nat, Nat, natural object , Nat, Nat, Nat] means (1 * $3) * ($1 !) = (1 * $2) - 1;
A8:
for n being Nat
for i1, i4, i2, i3, i5, i6 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S3[p . i1,p . i4,p . i2,p . i3,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT)
by A7;
deffunc H3( Nat, Nat, Nat) -> Element of omega = (1 * $1) + 1;
A9:
for n being Nat
for i1, i2, i3, i4 being Element of n holds { p where p is b1 -element XFinSequence of NAT : H3(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of (n -xtuples_of NAT)
by HILB10_3:15;
A10:
for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : S3[p . i1,p . i2,H3(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(A8, A9);
let n be Nat; for i1, i2, i3 being Element of n holds { p where p is n -element XFinSequence of NAT : 1 + (((p . i1) + 1) * ((p . i2) !)) = p . i3 } 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 : 1 + (((p . i1) + 1) * ((p . i2) !)) = p . i3 } is diophantine Subset of (n -xtuples_of NAT)
defpred S4[ XFinSequence of NAT ] means S3[$1 . i2,$1 . i3,(1 * ($1 . i1)) + 1,$1 . i3,$1 . i3,$1 . i3];
defpred S5[ XFinSequence of NAT ] means 1 + ((($1 . i1) + 1) * (($1 . i2) !)) = $1 . i3;
A11:
for p being n -element XFinSequence of NAT holds
( S4[p] iff S5[p] )
;
{ p where p is n -element XFinSequence of NAT : S4[p] } = { q where q is n -element XFinSequence of NAT : S5[q] }
from HILB10_3:sch 2(A11);
hence
{ p where p is n -element XFinSequence of NAT : 1 + (((p . i1) + 1) * ((p . i2) !)) = p . i3 } is diophantine Subset of (n -xtuples_of NAT)
by A10; verum