theorem LmSign1C: :: ZMODLAT2:48

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