let p be prime odd Nat; :: thesis: for m being positive Nat
for g being non zero Polynomial of INT.Ring holds delta_1 (m,p,g) is FinSequence of INT.Ring
let m be positive Nat; :: thesis: for g being non zero Polynomial of INT.Ring holds delta_1 (m,p,g) is FinSequence of INT.Ring
let g be non zero Polynomial of INT.Ring; :: thesis: delta_1 (m,p,g) is FinSequence of INT.Ring
rng (delta_1 (m,p,g)) c= the carrier of INT.Ring

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (delta_1 (m,p,g)) or x in the carrier of INT.Ring )
assume x in rng (delta_1 (m,p,g)) ; :: thesis: x in the carrier of INT.Ring
then consider z being object such that
A2: ( z in dom (delta_1 (m,p,g)) & x = (delta_1 (m,p,g)) . z ) by FUNCT_1:def 3;
len (delta_1 (m,p,g)) = m by Def5;
then A4: z in Seg m by A2, FINSEQ_1:def 3;
reconsider i0 = z as Nat by A2;
A5: ('F' (f_0 (m,p))) . (In (i0,F_Real)) in {(In ((p !),INT.Ring))} -Ideal by A4, Th34;
reconsider Ff = ('F' (f_0 (m,p))) . (In (i0,F_Real)) as Element of INT.Ring by A5;
(g . i0) * Ff is Element of INT.Ring ;
then (delta_1 (m,p,g)) . i0 is Element of INT.Ring by A2, Def5;
hence x in the carrier of INT.Ring by A2; :: thesis: verum

end;

hence delta_1 (m,p,g) is FinSequence of INT.Ring by FINSEQ_1:def 4; :: thesis: verum