theorem Th2: :: GR_CY_1:2

for I being FinSequence of INT holds Sum I = addint $$ I