theorem Th23: :: E_TRANS2:20

for p being prime odd Nat
for m being positive Nat holds eval ((~ (((Der1 INT.Ring) |^ (p -' 1)) . (f_0 (m,p)))),(0. INT.Ring)) = ((p -' 1) !) * (In (((((- 1) |^ m) * (m !)) |^ p),INT.Ring))