:: deftheorem defines Sum GR_CY_1:def 2 :
for I being FinSequence of INT holds Sum I = addint $$ I;