theorem Th29: :: E_TRANS2:26

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