let f be INT -valued FinSequence; :: thesis: for a being Integer st ( for n being Nat st n in dom f holds
a divides f . n ) holds
a divides Sum f
let a be Integer; :: thesis: ( ( for n being Nat st n in dom f holds
a divides f . n ) implies a divides Sum f )
assume A1: for n being Nat st n in dom f holds
a divides f . n ; :: thesis: a divides Sum f
reconsider f1 = f as FinSequence of REAL by NEWTON02:103;
f1 . (min_p f1) in INT by INT_1:def 2;
then reconsider k = min f1 as Integer by RFINSEQ2:def 4;
reconsider f2 = f as FinSequence of COMPLEX by NEWTON02:103;
reconsider g = f2 - k as FinSequence of INT by NEWTON02:103;
reconsider g = g as FinSequence of NAT by NEWTON02:103;
( |.a.| in INT & |.a.| >= 0 ) by INT_1:def 2;
then reconsider l = |.a.| as Nat ;
A1a: a divides k

proof

per cases ( min_p f1 in dom f1 or not min_p f1 in dom f1 ) ;

suppose B1: min_p f1 in dom f1 ; :: thesis: a divides k

reconsider x = min_p f1 as Nat ;
a divides f . x by B1, A1;
hence a divides k by RFINSEQ2:def 4; :: thesis: verum

end;

suppose not min_p f1 in dom f1 ; :: thesis: a divides k

then 0 = f1 . (min_p f1) by FUNCT_1:def 2
.= k by RFINSEQ2:def 4 ;
hence a divides k by INT_2:12; :: thesis: verum

end;

end;

end;

for m being Nat st m in dom g holds
l divides g . m

proof

let m be Nat; :: thesis: ( m in dom g implies l divides g . m )
assume B1: m in dom g ; :: thesis: l divides g . m
B2: m in dom (f2 + (- k)) by B1, VALUED_1:def 3;
then m in dom f by VALUED_1:def 2;
then ( a divides f . m & a divides - k ) by A1, A1a, INT_2:10;
then a divides (f . m) + (- k) by WSIERP_1:4;
then a divides (f + (- k)) . m by B2, VALUED_1:def 2;
then a divides (f - k) . m by VALUED_1:def 3;
hence l divides g . m by WSIERP_1:13; :: thesis: verum

end;

then A2: a divides Sum g by INT_4:36, WSIERP_1:13;
A3: a divides k * (len g) by A1a, INT_2:2;
reconsider g = g as FinSequence of COMPLEX by NEWTON02:103;
Sum (g + k) = (Sum g) + (k * (len g)) by SFX;
hence a divides Sum f by A2, A3, WSIERP_1:4; :: thesis: verum