theorem Th30: :: E_TRANS2:27

for p being prime odd Nat
for m being positive Nat
for k, j being Nat st j in Seg m & p <= k holds
ex u, v being Element of the carrier of (Polynom-Ring INT.Ring) st ((Der1 INT.Ring) |^ k) . (f_0 (m,p)) = ((tau j) * u) + ((p !) * v)