We can define pow by fixed-point construction and fixed-point induction. Here are those two axioms.

(pow fixed-point construction) pow = 1, 2×pow

(pow fixed-point induction) B = 1, 2×B ⇒ pow: B

These axioms do not use nat.

In Exercise 344, we are defining nat. We use

(nat fixed-point construction) nat = 0, nat+1

and either one of the two axioms given in the question. Let’s take part (a).

(a) ∀n: nat· 0 ≤ n < n+1

Since (a) is part of the definition of nat, it should mention nat, and it does. It seems to bother you that (a)'s use of nat is as a domain of quantification, but it can use it that way. It is indeed an unusual way to define nat. It is saying that nat is the bunch such that for all its elements n, 0 ≤ n < n+1.

To prove that (nat fixed-point construction) plus (a) together define nat, just use those two to prove the axioms we have previously used to define nat. Prove

(nat fixed-point construction) ∧ (a) ⇒ (nat fixed-point construction) ∧ (nat fixed-point induction)

And we can simplify that to

(nat fixed-point construction) ∧ (a) ⇒ (nat fixed-point induction)

For 344(b), Prove

(nat fixed-point construction) ∧ (b) ⇒ (nat fixed-point induction)

Or, after doing part (a), part (b) can be

(nat fixed-point construction) ∧ (b) ⇒ (a)