theorem Th27: :: ORDINAL5:27

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