for i2, i3, i4 being Element of F₁() holds { p where p is F₁() -element XFinSequence of NAT : for i being Nat st i in F₂() holds
P₁[p . i,p . i2,p . i3,p . i4] } is diophantine Subset of (F₁() -xtuples_of NAT)

A1: for i1, i2, i3, i4 being Element of F₁() holds { p where p is F₁() -element XFinSequence of NAT : P₁[p . i1,p . i2,p . i3,p . i4] } is diophantine Subset of (F₁() -xtuples_of NAT) and
A2: F₂() c= Segm F₁()