k >= 1 by NAT_1:14;
then ( n |^ k >= n or n < 1 ) by PREPOWER:12;
then ( (n |^ k) - n >= n - n or n = 0 ) by XREAL_1:9, NAT_1:14;
then (n |^ k) - n is Element of NAT by INT_1:3;
hence (n |^ k) - n is natural ; :: thesis: verum