theorem Th25: :: NAT_3:25

for a, b being Nat st 1 < b holds
b |-count (b |^ a) = a