scheme :: HILB10_3:sch 1
UnionDiophantine{ F1() -> Nat, P1[ XFinSequence of NAT ], P2[ XFinSequence of NAT ] } :
{ p where p is F1() -element XFinSequence of NAT : ( P1[p] or P2[p] ) } is diophantine Subset of (F1() -xtuples_of NAT)
provided
A1: { p where p is F1() -element XFinSequence of NAT : P1[p] } is diophantine Subset of (F1() -xtuples_of NAT) and
A2: { p where p is F1() -element XFinSequence of NAT : P2[p] } is diophantine Subset of (F1() -xtuples_of NAT)