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_{1} -element XFinSequence of NAT : p . i1 = (p . i2) -' 1 } is diophantine Subset of (n -xtuples_of NAT)

for i1, i2 being Element of n holds { p where p is b_{1} -element XFinSequence of NAT : p . i1 = ((p . i2) -' 1) ! } is diophantine Subset of (n -xtuples_of NAT)
_{1}[ Nat, Nat, natural object , Nat, Nat, Nat] means $4 = (1 * $3) + 1;

deffunc H_{1}( 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_{1} -element XFinSequence of NAT : S_{1}[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_{1} -element XFinSequence of NAT : H_{1}(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_{1} -element XFinSequence of NAT : S_{1}[p . i1,p . i2,H_{1}(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_{2}[ XFinSequence of NAT ] means $1 . i1 = (1 * ((($1 . i2) -' 1) !)) + 1;

defpred S_{3}[ XFinSequence of NAT ] means $1 . i1 = ((($1 . i2) -' 1) !) + 1;

A9: for q being n -element XFinSequence of NAT holds

( S_{2}[q] iff S_{3}[q] )
;

{ q where q is n -element XFinSequence of NAT : S_{2}[q] } = { r where r is n -element XFinSequence of NAT : S_{3}[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

A1: for n being Nat

for i1, i2 being Element of n holds { p where p is b

proof

A3:
for n being Nat
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_{1}[ XFinSequence of NAT ] means 1 * ($1 . i1) = (1 * ($1 . i2)) -' 1;

defpred S_{2}[ XFinSequence of NAT ] means $1 . i1 = ($1 . i2) -' 1;

A2: for q being n -element XFinSequence of NAT holds

( S_{1}[q] iff S_{2}[q] )
;

{ q where q is n -element XFinSequence of NAT : S_{1}[q] } = { r where r is n -element XFinSequence of NAT : S_{2}[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;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

defpred S

A2: for q being n -element XFinSequence of NAT holds

( S

{ q where q is n -element XFinSequence of NAT : S

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

for i1, i2 being Element of n holds { p where p is b

proof

defpred S
defpred S_{1}[ Nat, Nat, natural object , Nat, Nat, Nat] means $4 = $3 ! ;

deffunc H_{1}( 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_{1} -element XFinSequence of NAT : S_{1}[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_{1} -element XFinSequence of NAT : H_{1}(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_{1} -element XFinSequence of NAT : S_{1}[p . i1,p . i2,H_{1}(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_{1} -element XFinSequence of NAT : p . i1 = ((p . i2) -' 1) ! } is diophantine Subset of (n -xtuples_of NAT)
; :: thesis: verum

end;deffunc H

A4: for n being Nat

for i1, i2, i3, i4, i5, i6 being Element of n holds { p where p is b

A5: for n being Nat

for i1, i2, i3, i4 being Element of n holds { p where p is b

for n being Nat

for i1, i2, i3, i4, i5 being Element of n holds { p where p is b

hence for n being Nat

for i1, i2 being Element of n holds { p where p is b

deffunc H

A6: for n being Nat

for i1, i2, i3, i4, i5, i6 being Element of n holds { p where p is b

A7: for n being Nat

for i1, i2, i3, i4 being Element of n holds { p where p is b

A8: for n being Nat

for i1, i2, i3, i4, i5 being Element of n holds { p where p is b

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

defpred S

A9: for q being n -element XFinSequence of NAT holds

( S

{ q where q is n -element XFinSequence of NAT : S

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