As noted above, the disjointness of the sets sur i ( t ) 201 , A i and sur i ( t ′ ) 201 i , A i (for t ̸ = t ′ )
is required in order to ensure the existence of the bijection b. More precisely, in order to merge models 201, 202, the sets suri (t) 201, Ai for t member of some "relevant" subset of C 1 (Γ)
must form a partition of Wi's domain that satisfies a certain cardinality condition. This is formalized by the following definition:
Definition 46. Let κ be a cardinal. A set { X 1 , . . , X n } is called a κ -partition of a set W
iff 1. |Xi| = K, for all 1 < i < n, 2. X i N X i = 0 whenever i = j, and 3. W = U 1 <i <n X i .

{X 1 , . . . , X n } is a κ -partition of an ADM W with domain W iff it is a κ -partition of W .

In the proof, we will enforce that Properties 1 and 3 hold by appropriate constructions, while Property 2 holds by definition of C 1 (Γ).

Before proving Theorem 20, we repeat its formulation.

Theorem 20.  Let Si = (Li,Mi), i E {1,2}, be two local ADSs in which L1 is based on the set of function symbols F and relation symbols R, and L2 is based on G and Q, and let L = L 1 & L 2 and M = M 1 & M 2 . If Γ is a finite set of assertions from L , then the following are equivalent:
1. Γ is satisfiable in ( L , M ). 2. There exist
(a) a set D C C 1 (F),
(b) for every term t E D an object variable a t & obj ( Γ ),
(c) for every a E obj(F) a term t a E D,
ssssssssssse
(L1, M1):
(d) {a t : sur 1 (t) | t E D} U {T E sur 1 (VD)},
(c) {a : sur1(ta) | a E obj(F)},
(f) {R(a, b) | R(a, b) E Γ, R E R}, (g) { sur 1 (t 1 ) E sur 1 (t 2 ) | t 1 E t 2 E Γ} U { a : sur 1 (s) | (a : s) E Γ };
and the union Γ 2 of the following sets of assertions in L 2 is satisfiable in ( L 2 , M 2 ):
(h) {a t : sur2(t) { t E D} U {T E sur2(VD)},
(i) {a : sur2(ta) | a ∈ obj(Γ)},
(j) {Q(a, b) | Q(a, b) E Γ, Q E Q}.