for n, k being Nat holds exp (n,k) = n |^ k