let p be prime odd Nat; :: thesis: for m being positive Nat
for j being Nat st j in Seg m holds
Product (ff_0 (m,p)) = ((tau j) |^ p) * (Product (Del ((ff_0 (m,p)),j)))
let m be positive Nat; :: thesis: for j being Nat st j in Seg m holds
Product (ff_0 (m,p)) = ((tau j) |^ p) * (Product (Del ((ff_0 (m,p)),j)))
let j be Nat; :: thesis: ( j in Seg m implies Product (ff_0 (m,p)) = ((tau j) |^ p) * (Product (Del ((ff_0 (m,p)),j))) )
assume A1: j in Seg m ; :: thesis: Product (ff_0 (m,p)) = ((tau j) |^ p) * (Product (Del ((ff_0 (m,p)),j)))
then A2: j in dom (ff_0 (m,p)) by Lm7;
(tau j) |^ p = (ff_0 (m,p)) /. j by Lm7, A1;
hence Product (ff_0 (m,p)) = ((tau j) |^ p) * (Product (Del ((ff_0 (m,p)),j))) by A2, RATFUNC1:3; :: thesis: verum