let p be prime odd Nat; :: thesis: 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))
let m be positive Nat; :: thesis: 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))
let x be Element of F_Real; :: thesis: (Eval (~ (^ (f_0 (m,p))))) . x = (eval ((~ (^ (Product (x. (m,p))))),x)) * (eval ((~ (^ ((tau 0) |^ (p -' 1)))),x))
set Pxmp = Product (x. (m,p));
set tp1 = (tau 0) |^ (p -' 1);
~ (^ (f_0 (m,p))) = ~ (^ ((Product (x. (m,p))) * ((tau 0) |^ (p -' 1)))) by GROUP_4:6
.= ~ ((^ (Product (x. (m,p)))) * (^ ((tau 0) |^ (p -' 1)))) by E_TRANS1:27
.= (~ (^ (Product (x. (m,p))))) *' (~ (^ ((tau 0) |^ (p -' 1)))) by POLYNOM3:def 10 ;
then (Eval (~ (^ (f_0 (m,p))))) . x = eval (((~ (^ (Product (x. (m,p))))) *' (~ (^ ((tau 0) |^ (p -' 1))))),x) by POLYNOM5:def 13;
hence (Eval (~ (^ (f_0 (m,p))))) . x = (eval ((~ (^ (Product (x. (m,p))))),x)) * (eval ((~ (^ ((tau 0) |^ (p -' 1)))),x)) by POLYNOM4:24; :: thesis: verum