theorem Th8: :: INT_8:8

for m being Nat
for p being Prime st m >= 1 holds
Euler (p |^ m) = (p |^ m) - (p |^ (m -' 1))