:: deftheorem Def17 defines Partial_Sums SURREALC:def 17 :
for r being non-zero Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for b₃ being uSurreal-Sequence holds
( b₃ = Partial_Sums (r,y) iff ( dom b₃ = succ ((dom r) /\ (dom y)) & ( for A being Ordinal st A in dom b₃ holds
b₃,y,r simplest_on_position A ) ) );