deffunc H₁( 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 b₁ -element XFinSequence of NAT : H₁(p . i1,p . i2,p . i3) = a * (p . i4) } is diophantine Subset of (n -xtuples_of NAT) by HILB10_3:6;
defpred S₁[ 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 b₁ -element XFinSequence of NAT : S₁[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 b₁ -element XFinSequence of NAT : S₁[p . i1,p . i2,H₁(p . i3,p . i4,p . i5)] } is diophantine Subset of (n -xtuples_of NAT) from HILB10_3:sch 5(A2, A1);
deffunc H₂( 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 b₁ -element XFinSequence of NAT : H₂(p . i1,p . i2,p . i3) = p . i4 } is diophantine Subset of (n -xtuples_of NAT) by Th32;
defpred S₂[ Nat, Nat, natural object , Nat, Nat, Nat] means (1 * $1) * $3 = (1 * $2) - 1;

A5: now :: thesis: for n being Nat
for i1, i3, i2, i4, i5, i6 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : S₂[p . i1,p . i3,p . i2,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT)

let n be Nat; :: thesis: for i1, i3, i2, i4, i5, i6 being Element of n holds { p where p is n -element XFinSequence of NAT : S₂[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; :: thesis: { p where p is n -element XFinSequence of NAT : S₂[p . i1,p . i3,p . i2,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT)
defpred S₃[ XFinSequence of NAT ] means S₁[$1 . i1,$1 . i2,(1 * ($1 . i3)) + (- 1)];
defpred S₄[ XFinSequence of NAT ] means S₂[$1 . i1,$1 . i3,$1 . i2,$1 . i4,$1 . i5,$1 . i6];
A6: for p being n -element XFinSequence of NAT holds
( S₃[p] iff S₄[p] ) ;
{ p where p is n -element XFinSequence of NAT : S₃[p] } = { q where q is n -element XFinSequence of NAT : S₄[q] } from HILB10_3:sch 2(A6);
hence { p where p is n -element XFinSequence of NAT : S₂[p . i1,p . i3,p . i2,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT) by A3; :: thesis: verum

end;

A7: for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : S₂[p . i1,p . i2,H₂(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 S₃[ 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 b₁ -element XFinSequence of NAT : S₃[p . i1,p . i4,p . i2,p . i3,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT) by A7;
deffunc H₃( 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 b₁ -element XFinSequence of NAT : H₃(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 b₁ -element XFinSequence of NAT : S₃[p . i1,p . i2,H₃(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; :: thesis: 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; :: thesis: { 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 S₄[ XFinSequence of NAT ] means S₃[$1 . i2,$1 . i3,(1 * ($1 . i1)) + 1,$1 . i3,$1 . i3,$1 . i3];
defpred S₅[ XFinSequence of NAT ] means 1 + ((($1 . i1) + 1) * (($1 . i2) !)) = $1 . i3;
A11: for p being n -element XFinSequence of NAT holds
( S₄[p] iff S₅[p] ) ;
{ p where p is n -element XFinSequence of NAT : S₄[p] } = { q where q is n -element XFinSequence of NAT : S₅[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; :: thesis: verum