theorem Th33: :: E_TRANS2:30

for p being prime odd Nat
for m being positive Nat ex u being Element of INT.Ring st ('F' (f_0 (m,p))) . 0 = (((p -' 1) !) * (In (((((- 1) |^ m) * (m !)) |^ p),INT.Ring))) + ((In ((p !),INT.Ring)) * u)