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

A1: 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 : P₁[p . i1,p . i2,a * (p . i3)] } is diophantine Subset of (n -xtuples_of NAT) and
A2: 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 : F₁((p . i1),(p . i2),(p . i3)) = a * (p . i4) } is diophantine Subset of (n -xtuples_of NAT)