theorem Th34: :: E_TRANS2:31

for p being prime odd Nat
for m being positive Nat
for j being Nat st j in Seg m holds
('F' (f_0 (m,p))) . (In (j,F_Real)) in {(In ((p !),INT.Ring))} -Ideal