let r be non-zero Sequence of REAL ; :: thesis: for y being strictly_decreasing Surreal-Sequence holds Sum (r,y) in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y)
let y be strictly_decreasing Surreal-Sequence; :: thesis: Sum (r,y) in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y)
(dom r) /\ (dom y) in succ ((dom r) /\ (dom y)) by ORDINAL1:6;
then A1: (dom r) /\ (dom y) in dom (Partial_Sums (r,y)) by Def17;
Partial_Sums (r,y),y,r simplest_on_position (dom r) /\ (dom y) by A1, Def17;
hence Sum (r,y) in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y) ; :: thesis: verum