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