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,y)
let y be strictly_decreasing uSurreal-Sequence; :: thesis: ( dom r = dom y implies r,y, dom r name_like Sum (r,y) )
assume A1: dom r = dom y ; :: thesis: r,y, dom r name_like Sum (r,y)
thus ( dom r c= dom r & dom r = dom y ) by A1; :: according to SURREALC:def 19 :: thesis: for beta being Ordinal st beta in dom r holds
for Pb being Surreal st Pb = (Partial_Sums (r,y)) . beta holds
( not Sum (r,y) == Pb & r . beta = omega-r ((Sum (r,y)) - Pb) & y . beta = omega-y ((Sum (r,y)) - Pb) )
set P = Partial_Sums (r,y);
set s = Sum (r,y);
let beta be Ordinal; :: thesis: ( beta in dom r implies for Pb being Surreal st Pb = (Partial_Sums (r,y)) . beta holds
( not Sum (r,y) == Pb & r . beta = omega-r ((Sum (r,y)) - Pb) & y . beta = omega-y ((Sum (r,y)) - Pb) ) )
assume A2: beta in dom r ; :: thesis: for Pb being Surreal st Pb = (Partial_Sums (r,y)) . beta holds
( not Sum (r,y) == Pb & r . beta = omega-r ((Sum (r,y)) - Pb) & y . beta = omega-y ((Sum (r,y)) - Pb) )
let Pb be Surreal; :: thesis: ( Pb = (Partial_Sums (r,y)) . beta implies ( not Sum (r,y) == Pb & r . beta = omega-r ((Sum (r,y)) - Pb) & y . beta = omega-y ((Sum (r,y)) - Pb) ) )
assume A3: Pb = (Partial_Sums (r,y)) . beta ; :: thesis: ( not Sum (r,y) == Pb & r . beta = omega-r ((Sum (r,y)) - Pb) & y . beta = omega-y ((Sum (r,y)) - Pb) )
A4: dom (Partial_Sums (r,y)) = succ ((dom r) /\ (dom r)) by A1, Def17;
y . beta in rng y by A1, A2, FUNCT_1:def 3;
then reconsider yb = y . beta as uSurreal by SURREALO:def 12;
Partial_Sums (r,y),y,r simplest_on_position dom r by A4, Def17, ORDINAL1:6;
then Sum (r,y) in_meets_terms Partial_Sums (r,y),y,r, dom r by A1;
then A5: Sum (r,y) is Pb,yb,r . beta _term by A2, A3;
then A6: ( not (Sum (r,y)) + (- Pb) == 0_No & omega-y ((Sum (r,y)) + (- Pb)) == yb & omega-r ((Sum (r,y)) + (- Pb)) = r . beta ) ;
not Sum (r,y) == Pb

proof

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

end;

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