theorem Th35: :: E_TRANS2:32

for p being prime odd Nat
for m being positive Nat
for x being Element of F_Real holds (Eval (~ (^ (f_0 (m,p))))) . x = (eval ((~ (^ (Product (x. (m,p))))),x)) * (eval ((~ (^ ((tau 0) |^ (p -' 1)))),x))