let p be prime odd Nat; :: thesis: for x being Element of F_Real holds eval ((~ (^ ((tau 0) |^ (p -' 1)))),x) = x |^ (p -' 1)
let x be Element of F_Real; :: thesis: eval ((~ (^ ((tau 0) |^ (p -' 1)))),x) = x |^ (p -' 1)
set t0 = <%(In ((- 0),F_Real)),(1. F_Real)%>;
reconsider u0 = tau 0 as Polynomial of F_Real by FIELD_4:8;
A1: eval (u0,x) = eval (<%(In ((- 0),F_Real)),(1. F_Real)%>,x)
.= (0. F_Real) + ((1. F_Real) * x) by POLYNOM5:44
.= x ;
set p1 = p -' 1;
eval ((~ (^ ((tau 0) |^ (p -' 1)))),x) = eval ((~ ((^ (tau 0)) |^ (p -' 1))),x) by Th4
.= eval (((~ (^ (tau 0))) `^ (p -' 1)),x) by Th5
.= (power F_Real) . (x,(p -' 1)) by POLYNOM5:22, A1 ;
hence eval ((~ (^ ((tau 0) |^ (p -' 1)))),x) = x |^ (p -' 1) by BINOM:def 2; :: thesis: verum