for F being FinSequence of F_Real st ( for i being Nat st i in dom F holds
F . i in INT ) holds
Sum F in INT