∀ a.∀ n.( (<(z,a)∧¬(a=z)∧Nat(n)) → ∃ b. ((<(z,b)∧¬(b=z)∧exp(b,n)=a) ∧∀ c.((<(z,c)∧¬(c=z)∧exp(c,n)=a) → c=a)))