theorem Th26: :: E_TRANS2:23

for p being prime odd Nat
for m being positive Nat
for k, j being Nat st k < p & j in Seg m holds
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(In (j,INT.Ring))) = 0. INT.Ring