exp (n,k) = n |^ k by LemExp;
hence exp (n,k) is natural ; :: thesis: verum