scheme :: HILB10_3:sch 1
UnionDiophantine{ F₁() -> Nat, P₁[ XFinSequence of NAT ], P₂[ XFinSequence of NAT ] } :

{ p where p is F₁() -element XFinSequence of NAT : ( P₁[p] or P₂[p] ) } is diophantine Subset of (F₁() -xtuples_of NAT)

provided

A1: { p where p is F₁() -element XFinSequence of NAT : P₁[p] } is diophantine Subset of (F₁() -xtuples_of NAT) and
A2: { p where p is F₁() -element XFinSequence of NAT : P₂[p] } is diophantine Subset of (F₁() -xtuples_of NAT)