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