:: deftheorem defines Sum SERIES_1:def 3 :
for s being Real_Sequence holds Sum s = lim (Partial_Sums s);