theorem Th24: :: E_TRANS2:21

for p being prime odd Nat
for m being positive Nat
for k being non zero Nat st p <= k holds
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(0. INT.Ring)) = (k !) * ((~ (Product (x. (m,p)))) . (k -' (p -' 1)))