theorem th0e: :: FIELD_5:4

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