We repeat the formulation of the theorem to be proved.

Theorem 30. Let Si = (Li, Mi), i E {1, 2}, be two local ADSs having covering normal terms in which L1 is based on the set of function symbols F and relation symbols R, and L 2 is based on G and Q, and let L = L 1 & L 2 and M = M 1 & M 2 . Let Γ be a finite set of object assertions from L . Put m := d F (Γ), r := d G (Γ), and let c(x) (d(x)) be a covering normal term for all function symbols in Γ that are in F (G).

For i E {1,2}, denote by Σ i the set of all s ∈ C i (Γ) such that the term s is satisfiable in
(L, M). Then the following three conditions are equivalent:
1. Γ is satisfiable in (L, M).

2. There exist
- for every t E Σ 1 an object variable a ξ ξ obj (Γ) - for every a E obj(F) a term t a E E1 such that the union Γ 1 of the following sets of object assertions is satisfiable in
(L1, M1):
- {at : sur1(t Ac<m(sur1(VE1)) | t E Σ1},

- { a : sur 1 ( t a ∧ c ≤ m ( sur 1 ( √ Σ 1 )) | a ∈ obj ( Γ )},
- {R(a, b) | R(a, b) ∈ Γ, R ∈ R},
- {a : sur1 (s) | (a : s) E F};
and the union Γ 2 of the following sets of object assertions is satisfiable in ( L 2 , M 2 ):
- {at : sur2(t A d<r(sur2(V E1)) | t E E1},

- { a : sur2 ( t a ∧ d ≤ r ( sur2 ( V Σ 1 )) | a ∈ obj ( Γ )},
- {Q(a, b) | Q(a, b) E Γ, Q E Q}.
3. The same condition as in (2) above, with E1 replaced by E2.

We start the proof with the direction from (1) to (2) and (1) to (3). The proofs are dual to each other, so we only give a proof for (1) ⇒ (2).  Suppose (20, A) |= Γ, where W = (W, (F U G) W, (R U Q) W). By Lemma 45, we can assume that that, for every t E Σ 1 ,
| t 20, A | is infinite. Take a new object name a s & obj ( Γ ) for every s ∈ Σ 1 and let, for a E obj(F),

## T A = N { T E Sub 1 (Γ) : A 2 (Α) E T 2 V, A } ∧ {¬T : T E Sub 1 (Γ), A 2 (Α) & T 2 V, A } .

We prove that the set Γ 1 of assertions based on t α , a ∈ o bj (Γ), and α s, s ∈ Σ 1 , is satisfiable in ( L 1 , M 1 ) (the proof is rather similar to the proof of the direction from (1) to (2) in the proof of Theorem 20). Let F 20 (resp. G 20 ) denote the restriction of ( F UG ) 201 to the symbols in F (resp. G ). Similarly, R 2 p and Q 2 p are the restrictions of ( R ∪ Q ) 2 p to the symbols in R and Q, respectively. Set 201 = (W, F20, R20) E M1, A1 = (A), A1), where A 1 = A 1 U { x t → t 20,A | t = g( t 1 , . . , t k ) E sub 1 ( Γ )},