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 INT.Ring
let m be positive Nat; :: thesis: for g being non zero Polynomial of INT.Ring holds Sum (delta_1 (m,p,g)) in INT.Ring
let g be non zero Polynomial of INT.Ring; :: thesis: Sum (delta_1 (m,p,g)) in INT.Ring
for i being Nat st i in dom (delta_1 (m,p,g)) holds
(delta_1 (m,p,g)) . i in INT

proof

let i be Nat; :: thesis: ( i in dom (delta_1 (m,p,g)) implies (delta_1 (m,p,g)) . i in INT )
assume i in dom (delta_1 (m,p,g)) ; :: thesis: (delta_1 (m,p,g)) . i in INT
then A2: (delta_1 (m,p,g)) . i = (g . i) * (('F' (f_0 (m,p))) . (In (i,F_Real))) by Def5;
reconsider r = i as Element of F_Real by XREAL_0:def 1;
reconsider i0 = i as Element of INT.Ring by INT_1:def 2;
('F' (f_0 (m,p))) . (In (i,F_Real)) = Sum (eval (('G' (f_0 (m,p))),i0)) by E_TRANS1:30;
hence (delta_1 (m,p,g)) . i in INT by A2, INT_1:def 2; :: thesis: verum

end;

hence Sum (delta_1 (m,p,g)) in INT.Ring by ZMATRLIN:42; :: thesis: verum