let p be prime odd Nat; :: thesis: for m being positive Nat
for g being non zero Polynomial of INT.Ring holds Sum (delta_1 (m,p,g)) in {(In ((p !),INT.Ring))} -Ideal
let m be positive Nat; :: thesis: for g being non zero Polynomial of INT.Ring holds Sum (delta_1 (m,p,g)) in {(In ((p !),INT.Ring))} -Ideal
let g be non zero Polynomial of INT.Ring; :: thesis: Sum (delta_1 (m,p,g)) in {(In ((p !),INT.Ring))} -Ideal
for i being Nat st i in dom (^delta (m,p,g)) holds
(^delta (m,p,g)) . i in {(In ((p !),INT.Ring))} -Ideal

proof

let i be Nat; :: thesis: ( i in dom (^delta (m,p,g)) implies (^delta (m,p,g)) . i in {(In ((p !),INT.Ring))} -Ideal )
assume A1: i in dom (^delta (m,p,g)) ; :: thesis: (^delta (m,p,g)) . i in {(In ((p !),INT.Ring))} -Ideal
len (^delta (m,p,g)) = m by Def5;
then A2: i in Seg m by A1, FINSEQ_1:def 3;
then ('F' (f_0 (m,p))) . (In (i,F_Real)) in {(In ((p !),INT.Ring))} -Ideal by Th34;
then reconsider Ff = ('F' (f_0 (m,p))) . (In (i,F_Real)) as Element of INT.Ring ;
(g . i) * Ff in {(In ((p !),INT.Ring))} -Ideal by A2, Th34, IDEAL_1:def 2;
hence (^delta (m,p,g)) . i in {(In ((p !),INT.Ring))} -Ideal by A1, Def5; :: thesis: verum

end;

then Sum (^delta (m,p,g)) in {(In ((p !),INT.Ring))} -Ideal by E_TRANS1:3;
hence Sum (delta_1 (m,p,g)) in {(In ((p !),INT.Ring))} -Ideal by LIOUVIL2:5, FIELD_4:2; :: thesis: verum