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