let n be Nat; :: thesis: for i, j being Element of n holds { p where p is n -element XFinSequence of NAT : p . i = (((p . j) -' 1) !) + 1 } is diophantine Subset of (n -xtuples_of NAT)
A1: for n being Nat
for i1, i2 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : p . i1 = (p . i2) -' 1 } is diophantine Subset of (n -xtuples_of NAT)

proof

let n be Nat; :: thesis: for i1, i2 being Element of n holds { p where p is n -element XFinSequence of NAT : p . i1 = (p . i2) -' 1 } is diophantine Subset of (n -xtuples_of NAT)
let i1, i2 be Element of n; :: thesis: { p where p is n -element XFinSequence of NAT : p . i1 = (p . i2) -' 1 } is diophantine Subset of (n -xtuples_of NAT)
defpred S₁[ XFinSequence of NAT ] means 1 * ($1 . i1) = (1 * ($1 . i2)) -' 1;
defpred S₂[ XFinSequence of NAT ] means $1 . i1 = ($1 . i2) -' 1;
A2: for q being n -element XFinSequence of NAT holds
( S₁[q] iff S₂[q] ) ;
{ q where q is n -element XFinSequence of NAT : S₁[q] } = { r where r is n -element XFinSequence of NAT : S₂[r] } from HILB10_3:sch 2(A2);
hence { p where p is n -element XFinSequence of NAT : p . i1 = (p . i2) -' 1 } is diophantine Subset of (n -xtuples_of NAT) by HILB10_3:20; :: thesis: verum

end;

A3: for n being Nat
for i1, i2 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : p . i1 = ((p . i2) -' 1) ! } is diophantine Subset of (n -xtuples_of NAT)

proof

defpred S₁[ Nat, Nat, natural object , Nat, Nat, Nat] means $4 = $3 ! ;
deffunc H₁( Nat, Nat, Nat) -> Element of omega = $2 -' 1;
A4: for n being Nat
for i1, i2, i3, i4, i5, i6 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : S₁[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT) by HILB10_4:32;
A5: 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 A1;
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(A4, A5);
hence for n being Nat
for i1, i2 being Element of n holds { p where p is b₁ -element XFinSequence of NAT : p . i1 = ((p . i2) -' 1) ! } is diophantine Subset of (n -xtuples_of NAT) ; :: thesis: verum

end;

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