let r be non-zero Sequence of REAL ; :: thesis: for y being strictly_decreasing Surreal-Sequence holds (dom r) /\ (dom y) c= born (Sum (r,y))
let y be strictly_decreasing Surreal-Sequence; :: thesis: (dom r) /\ (dom y) c= born (Sum (r,y))
set s = Partial_Sums (r,y);
A1: dom (Partial_Sums (r,y)) = succ ((dom r) /\ (dom y)) by Def17;
( Sum (r,y) in_meets_terms Partial_Sums (r,y),y,r,(dom r) /\ (dom y) & Partial_Sums (r,y),y,r simplest_up_to dom (Partial_Sums (r,y)) ) by Def17, Th89;
then A2: rng (born ((Partial_Sums (r,y)) | (dom (Partial_Sums (r,y))))) c= succ (born_eq (Sum (r,y))) by XBOOLE_1:17, Th98, A1;
A3: born_eq (Sum (r,y)) = born (Sum (r,y)) by SURREALO:48;
succ ((dom r) /\ (dom y)) c= succ (born (Sum (r,y)))

proof

let o be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not o in succ ((dom r) /\ (dom y)) or o in succ (born (Sum (r,y))) )
assume A4: o in succ ((dom r) /\ (dom y)) ; :: thesis: o in succ (born (Sum (r,y)))
A5: o in dom (Partial_Sums (r,y)) by A4, Def17;
then (Partial_Sums (r,y)) . o in rng (Partial_Sums (r,y)) by FUNCT_1:def 3;
then reconsider so = (Partial_Sums (r,y)) . o as uSurreal by SURREALO:def 12;
A6: dom (born (Partial_Sums (r,y))) = dom (Partial_Sums (r,y)) by Def20;
A7: born so = (born (Partial_Sums (r,y))) . o by A5, Def20;
then A8: born so in rng (born (Partial_Sums (r,y))) by A6, A5, FUNCT_1:def 3;
o c= (born (Partial_Sums (r,y))) . o by A5, A6, ORDINAL4:10;
hence o in succ (born (Sum (r,y))) by A7, A8, A2, A3, ORDINAL1:12; :: thesis: verum

end;

then (dom r) /\ (dom y) in succ (born (Sum (r,y))) by ORDINAL1:21;
hence (dom r) /\ (dom y) c= born (Sum (r,y)) by ORDINAL1:22; :: thesis: verum