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