theorem Th3: :: HILB10_6:3

for n being Nat
for i being Element of n holds { p where p is b₁ -element XFinSequence of NAT : ( ((((p . i) -' 1) !) + 1) mod (p . i) = 0 & p . i > 1 ) } is diophantine Subset of (n -xtuples_of NAT)