theorem Th7: :: NUMBER11:7

for n, b being Nat st b > 1 holds
value ((n --> (b -' 1)),b) = (b |^ n) - 1