theorem Th22: :: E_TRANS2:19

for p being prime odd Nat
for m being positive Nat
for k being Nat st 0 <= k & k <= p -' 2 holds
eval ((~ (((Der1 INT.Ring) |^ k) . (f_0 (m,p)))),(0. INT.Ring)) = 0. INT.Ring