theorem Th21: :: E_TRANS2:18

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