let r be non-zero Sequence of REAL ; :: thesis: for y being strictly_decreasing uSurreal-Sequence
for A being Ordinal st A c= dom r & dom r = dom y holds
for x, z being Surreal st r,y,A name_like x & x == z holds
r,y,A name_like z
let y be strictly_decreasing uSurreal-Sequence; :: thesis: for A being Ordinal st A c= dom r & dom r = dom y holds
for x, z being Surreal st r,y,A name_like x & x == z holds
r,y,A name_like z
let A be Ordinal; :: thesis: ( A c= dom r & dom r = dom y implies for x, z being Surreal st r,y,A name_like x & x == z holds
r,y,A name_like z )
assume ( A c= dom r & dom r = dom y ) ; :: thesis: for x, z being Surreal st r,y,A name_like x & x == z holds
r,y,A name_like z
let x, z be Surreal; :: thesis: ( r,y,A name_like x & x == z implies r,y,A name_like z )
assume A2: ( r,y,A name_like x & x == z ) ; :: thesis: r,y,A name_like z
thus ( A c= dom r & dom r = dom y ) by A2; :: according to SURREALC:def 19 :: thesis: for beta being Ordinal st beta in A holds
for Pb being Surreal st Pb = (Partial_Sums (r,y)) . beta holds
( not z == Pb & r . beta = omega-r (z - Pb) & y . beta = omega-y (z - Pb) )
let B be Ordinal; :: thesis: ( B in A implies for Pb being Surreal st Pb = (Partial_Sums (r,y)) . B holds
( not z == Pb & r . B = omega-r (z - Pb) & y . B = omega-y (z - Pb) ) )
assume A3: B in A ; :: thesis: for Pb being Surreal st Pb = (Partial_Sums (r,y)) . B holds
( not z == Pb & r . B = omega-r (z - Pb) & y . B = omega-y (z - Pb) )
let Pb be Surreal; :: thesis: ( Pb = (Partial_Sums (r,y)) . B implies ( not z == Pb & r . B = omega-r (z - Pb) & y . B = omega-y (z - Pb) ) )
assume A4: Pb = (Partial_Sums (r,y)) . B ; :: thesis: ( not z == Pb & r . B = omega-r (z - Pb) & y . B = omega-y (z - Pb) )
thus not z == Pb by A2, A3, A4, SURREALO:10; :: thesis: ( r . B = omega-r (z - Pb) & y . B = omega-y (z - Pb) )
A5: x - Pb == z - Pb by A2, SURREALR:66;
A6: ( not x == Pb & r . B = omega-r (x - Pb) & y . B = omega-y (x - Pb) ) by A2, A3, A4;
then not x - Pb == 0_No by SURREALR:45, SURREALR:46;
hence ( r . B = omega-r (z - Pb) & y . B = omega-y (z - Pb) ) by A5, A6, Th70; :: thesis: verum