theorem Th4: :: UNIROOTS:4

for f being FinSequence of F_Complex st ( for i being Element of NAT st i in dom f holds
f . i is integer ) holds
Sum f is integer