scheme :: HILB10_3:sch 4
Substitution{ P1[ Nat, Nat, natural object , Nat, Nat, Nat], F1( Nat, Nat, Nat) -> natural object } :
for n being Nat
for i1, i2, i3, i4, i5 being Element of n holds { p where p is b1 -element XFinSequence of NAT : P1[p . i1,p . i2,F1((p . i3),(p . i4),(p . i5)),p . i3,p . i4,p . i5] } is diophantine Subset of (n -xtuples_of NAT)
provided
A1: 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 : P1[p . i1,p . i2,p . i3,p . i4,p . i5,p . i6] } is diophantine Subset of (n -xtuples_of NAT) and
A2: for n being Nat
for i1, i2, i3, i4 being Element of n holds { p where p is b1 -element XFinSequence of NAT : F1((p . i1),(p . i2),(p . i3)) = p . i4 } is diophantine Subset of (n -xtuples_of NAT)