Prove:

under the assumptions:

We assume

and show

Formula (1.1), by (Definition (limit:)), implies:

By (3), we can take an appropriate Skolem function such that

Formula (1.2), by (Definition (limit:)), implies:

By (5), we can take an appropriate Skolem function such that

Formula (2), using (Definition (limit:)), is implied by:

We assume

and show

We have to find such that

Formula (10), using (Definition (+:)), is implied by:

Formula (11), using (Lemma(|+|)), is implied by:

We have to find , and such that

Formula (13), using (6), is implied by:

which, using (4), is implied by:

which, using (Lemma (max)), is implied by:

Formula (14) is implied by:

Partially solving it, formula (15) is implied by:

Now,

can be solved for and by a call to Collins' CAD method yielding the solution

Let us take

Formula (16) is solved. Hence, we are done.