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