theorem LmSign1C: :: ZMATRLIN:42

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