theorem Th40: :: E_TRANS2:37

for p being prime odd Nat
for x being Element of F_Real holds eval ((~ (^ ((tau 0) |^ (p -' 1)))),x) = x |^ (p -' 1)