let r be non-zero Sequence of REAL ; :: thesis: for y being strictly_decreasing uSurreal-Sequence st dom r = dom y holds
r,y, dom r name_like Sum (r,(No_omega^ y))
let y be strictly_decreasing uSurreal-Sequence; :: thesis: ( dom r = dom y implies r,y, dom r name_like Sum (r,(No_omega^ y)) )
assume A1: dom r = dom y ; :: thesis: r,y, dom r name_like Sum (r,(No_omega^ y))
thus ( dom r c= dom r & dom r = dom y ) by A1; :: according to SURREALC:def 23 :: thesis: for beta being Ordinal st beta in dom r holds
for Pb being Surreal st Pb = (Partial_Sums (r,(No_omega^ y))) . beta holds
( not Sum (r,(No_omega^ y)) == Pb & r . beta = omega-r ((Sum (r,(No_omega^ y))) - Pb) & y . beta = omega-y ((Sum (r,(No_omega^ y))) - Pb) )
set P = Partial_Sums (r,(No_omega^ y));
set s = Sum (r,(No_omega^ y));
A2: dom y = dom (No_omega^ y) by Def22;
let beta be Ordinal; :: thesis: ( beta in dom r implies for Pb being Surreal st Pb = (Partial_Sums (r,(No_omega^ y))) . beta holds
( not Sum (r,(No_omega^ y)) == Pb & r . beta = omega-r ((Sum (r,(No_omega^ y))) - Pb) & y . beta = omega-y ((Sum (r,(No_omega^ y))) - Pb) ) )
assume A3: beta in dom r ; :: thesis: for Pb being Surreal st Pb = (Partial_Sums (r,(No_omega^ y))) . beta holds
( not Sum (r,(No_omega^ y)) == Pb & r . beta = omega-r ((Sum (r,(No_omega^ y))) - Pb) & y . beta = omega-y ((Sum (r,(No_omega^ y))) - Pb) )
let Pb be Surreal; :: thesis: ( Pb = (Partial_Sums (r,(No_omega^ y))) . beta implies ( not Sum (r,(No_omega^ y)) == Pb & r . beta = omega-r ((Sum (r,(No_omega^ y))) - Pb) & y . beta = omega-y ((Sum (r,(No_omega^ y))) - Pb) ) )
assume A4: Pb = (Partial_Sums (r,(No_omega^ y))) . beta ; :: thesis: ( not Sum (r,(No_omega^ y)) == Pb & r . beta = omega-r ((Sum (r,(No_omega^ y))) - Pb) & y . beta = omega-y ((Sum (r,(No_omega^ y))) - Pb) )
A5: dom (Partial_Sums (r,(No_omega^ y))) = succ ((dom r) /\ (dom r)) by A1, A2, Def20;
y . beta in rng y by A1, A3, FUNCT_1:def 3;
then reconsider yb = y . beta as uSurreal by SURREALO:def 12;
A6: (No_omega^ y) . beta = No_omega^ yb by Def22, A1, A2, A3;
A7: r . beta in rng r by A3, FUNCT_1:def 3;
Partial_Sums (r,(No_omega^ y)), No_omega^ y,r simplest_on_position dom r by A5, Def20, ORDINAL1:6;
then Sum (r,(No_omega^ y)) in_meets_terms Partial_Sums (r,(No_omega^ y)), No_omega^ y,r, dom r by A1, A2;
then Sum (r,(No_omega^ y)) is Pb, No_omega^ yb,r . beta _Term by A3, A4, A6;
then A8: Sum (r,(No_omega^ y)) is Pb,yb,r . beta _term by A7, Th73;
then A9: ( not (Sum (r,(No_omega^ y))) + (- Pb) == 0_No & omega-y ((Sum (r,(No_omega^ y))) + (- Pb)) == yb & omega-r ((Sum (r,(No_omega^ y))) + (- Pb)) = r . beta ) ;
not Sum (r,(No_omega^ y)) == Pb

proof

assume Sum (r,(No_omega^ y)) == Pb ; :: thesis: contradiction
then ( (Sum (r,(No_omega^ y))) + (- Pb) == Pb - Pb & Pb - Pb == 0_No ) by SURREALR:43, SURREALR:39;
hence contradiction by A9, SURREALO:4; :: thesis: verum

end;

hence ( not Sum (r,(No_omega^ y)) == Pb & r . beta = omega-r ((Sum (r,(No_omega^ y))) - Pb) & y . beta = omega-y ((Sum (r,(No_omega^ y))) - Pb) ) by A8, SURREALO:50; :: thesis: verum