theorem Th32: :: E_TRANS2:29

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