set D = (dom r) /\ (dom y);
(dom r) /\ (dom y) in succ ((dom r) /\ (dom y)) by ORDINAL1:6;
then (dom r) /\ (dom y) in dom (Partial_Sums (r,y)) by Def17;
then A1: (Partial_Sums (r,y)) . ((dom r) /\ (dom y)) in rng (Partial_Sums (r,y)) by FUNCT_1:def 3;
rng (Partial_Sums (r,y)) is uniq-surreal-membered ;
hence (Partial_Sums (r,y)) . ((dom r) /\ (dom y)) is uSurreal by A1; :: thesis: verum