 The first clause of the theorem below, in this particular instance, says that the formula \(A\) above is derivable in first-order logic if and only if there is a sequence of terms \(t_{1}^1, t_{3}^1, \ldots, t_{1}^n, t_{3}^n\) in the expanded language with \(f_2\) and \(f_4\)  such that \[ B(t_{1}^1, f_2 (t_{1}^1), t_{3}^1, f_4 (t_{1}^1,t_{3}^1)) \vee \ldots \vee B(t_{1}^n, f_2 (t_{1}^n), t_{3}^n, f_4 (t_{1}^n,t_{3}^n)) \] is a quasi-tautology.