theorem Th13: :: E_TRANS1:3

for L being comRing
for I being Ideal of L
for F being FinSequence of L st ( for i being Nat st i in dom F holds
F . i in I ) holds
Sum F in I