:: deftheorem defines Sum SURREALC:def 18 :
for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence holds Sum (r,y) = (Partial_Sums (r,y)) . ((dom r) /\ (dom y));