theorem Th28: :: E_TRANS2:25

for p being prime odd Nat
for m being positive Nat
for j, k being Nat st j in Seg m & p <= k holds
for i being Nat st i in Seg p holds
tau j divides (LBZ ((Der1 INT.Ring),k,(Product (Del ((ff_0 (m,p)),j))),((tau j) |^ p))) /. i