let r be Sequence of REAL ; :: thesis: for y1, y2 being strictly_decreasing Surreal-Sequence
for A being Ordinal st A c= (dom r) /\ (dom y1) & dom y1 = dom y2 & ( for B being Ordinal st B in A holds
y1 .. B == y2 .. B ) holds
Sum ((r | A),((No_omega^ y1) | A)) = Sum ((r | A),((No_omega^ y2) | A))
let y1, y2 be strictly_decreasing Surreal-Sequence; :: thesis: for A being Ordinal st A c= (dom r) /\ (dom y1) & dom y1 = dom y2 & ( for B being Ordinal st B in A holds
y1 .. B == y2 .. B ) holds
Sum ((r | A),((No_omega^ y1) | A)) = Sum ((r | A),((No_omega^ y2) | A))
let O be Ordinal; :: thesis: ( O c= (dom r) /\ (dom y1) & dom y1 = dom y2 & ( for B being Ordinal st B in O holds
y1 .. B == y2 .. B ) implies Sum ((r | O),((No_omega^ y1) | O)) = Sum ((r | O),((No_omega^ y2) | O)) )
assume that
A1: O c= (dom r) /\ (dom y1) and
A2: dom y1 = dom y2 and
A3: for X being Ordinal st X in O holds
y1 .. X == y2 .. X ; :: thesis: Sum ((r | O),((No_omega^ y1) | O)) = Sum ((r | O),((No_omega^ y2) | O))
set N1 = No_omega^ y1;
set N2 = No_omega^ y2;
defpred S1[ Ordinal] means ( $1 c= O implies Sum ((r | $1),((No_omega^ y1) | $1)) = Sum ((r | $1),((No_omega^ y2) | $1)) );
A4: ( dom (No_omega^ y1) = dom y1 & dom (No_omega^ y2) = dom y2 ) by SURREALC:def 22;
A5: for B being Ordinal st B in O holds
(No_omega^ y1) .. B == (No_omega^ y2) .. B
proof
let B be Ordinal; :: thesis: ( B in O implies (No_omega^ y1) .. B == (No_omega^ y2) .. B )
assume A6: B in O ; :: thesis: (No_omega^ y1) .. B == (No_omega^ y2) .. B
A7: B in dom y1 by A1, A6, XBOOLE_0:def 4;
then ( y1 . B = y1 .. B & y2 . B = y2 .. B ) by A2, Def5;
then A8: ( (No_omega^ y1) . B = No_omega^ (y1 .. B) & (No_omega^ y2) . B = No_omega^ (y2 .. B) ) by A2, A4, A7, SURREALC:def 22;
A9: y1 .. B == y2 .. B by A6, A3;
( (No_omega^ y1) . B = (No_omega^ y1) .. B & (No_omega^ y2) . B = (No_omega^ y2) .. B ) by A2, A7, A4, Def5;
hence (No_omega^ y1) .. B == (No_omega^ y2) .. B by A8, A9, SURREALC:24; :: thesis: verum
end;
A10: for A being Ordinal st ( for C being Ordinal st C in A holds
S1[C] ) holds
S1[A]
proof
let A be Ordinal; :: thesis: ( ( for C being Ordinal st C in A holds
S1[C] ) implies S1[A] )
assume A11: for C being Ordinal st C in A holds
S1[C] ; :: thesis: S1[A]
assume A12: A c= O ; :: thesis: Sum ((r | A),((No_omega^ y1) | A)) = Sum ((r | A),((No_omega^ y2) | A))
then A13: A c= (dom r) /\ (dom y1) by A1;
reconsider X1 = [ { ((Sum ((r | B),((No_omega^ y1) | B))) + ((uReal . ((r . B) - e)) * ((No_omega^ y1) .. B))) where B is Element of A, e is positive Real : B in A } , { ((Sum ((r | B),((No_omega^ y1) | B))) + ((uReal . ((r . B) + e)) * ((No_omega^ y1) .. B))) where B is Element of A, e is positive Real : B in A } ] as Surreal by A13, A4, Th61;
reconsider X2 = [ { ((Sum ((r | B),((No_omega^ y2) | B))) + ((uReal . ((r . B) - e)) * ((No_omega^ y2) .. B))) where B is Element of A, e is positive Real : B in A } , { ((Sum ((r | B),((No_omega^ y2) | B))) + ((uReal . ((r . B) + e)) * ((No_omega^ y2) .. B))) where B is Element of A, e is positive Real : B in A } ] as Surreal by A13, A2, A4, Th61;
A14: L_ X1 <==> L_ X2
proof
thus L_ X1 <=_ L_ X2 :: according to SURREALO:def 4 :: thesis: L_ X2 <=_ L_ X1
proof
let x be Surreal; :: according to SURREALO:def 3 :: thesis: ( not x in L_ X1 or ex b1, b2 being set st
( b1 in L_ X2 & b2 in L_ X2 & b1 <= x & x <= b2 ) )
assume x in L_ X1 ; :: thesis: ex b1, b2 being set st
( b1 in L_ X2 & b2 in L_ X2 & b1 <= x & x <= b2 )
then consider B being Element of A, e being positive Real such that
A15: ( x = (Sum ((r | B),((No_omega^ y1) | B))) + ((uReal . ((r . B) - e)) * ((No_omega^ y1) .. B)) & B in A ) ;
B c= O by A12, A15, ORDINAL1:10;
then A16: Sum ((r | B),((No_omega^ y1) | B)) = Sum ((r | B),((No_omega^ y2) | B)) by A11, A15;
(uReal . ((r . B) - e)) * ((No_omega^ y1) .. B) == (uReal . ((r . B) - e)) * ((No_omega^ y2) .. B) by A12, A15, A5, SURREALR:54;
then ( x == (Sum ((r | B),((No_omega^ y2) | B))) + ((uReal . ((r . B) - e)) * ((No_omega^ y2) .. B)) & (Sum ((r | B),((No_omega^ y2) | B))) + ((uReal . ((r . B) - e)) * ((No_omega^ y2) .. B)) in L_ X2 ) by A15, A16, SURREALR:66;
hence ex b1, b2 being set st
( b1 in L_ X2 & b2 in L_ X2 & b1 <= x & x <= b2 ) ; :: thesis: verum
end;
let x be Surreal; :: according to SURREALO:def 3 :: thesis: ( not x in L_ X2 or ex b1, b2 being set st
( b1 in L_ X1 & b2 in L_ X1 & b1 <= x & x <= b2 ) )
assume x in L_ X2 ; :: thesis: ex b1, b2 being set st
( b1 in L_ X1 & b2 in L_ X1 & b1 <= x & x <= b2 )
then consider B being Element of A, e being positive Real such that
A17: ( x = (Sum ((r | B),((No_omega^ y2) | B))) + ((uReal . ((r . B) - e)) * ((No_omega^ y2) .. B)) & B in A ) ;
B c= O by A12, A17, ORDINAL1:10;
then A18: Sum ((r | B),((No_omega^ y1) | B)) = Sum ((r | B),((No_omega^ y2) | B)) by A11, A17;
(uReal . ((r . B) - e)) * ((No_omega^ y1) .. B) == (uReal . ((r . B) - e)) * ((No_omega^ y2) .. B) by A12, A17, A5, SURREALR:54;
then ( x == (Sum ((r | B),((No_omega^ y1) | B))) + ((uReal . ((r . B) - e)) * ((No_omega^ y1) .. B)) & (Sum ((r | B),((No_omega^ y1) | B))) + ((uReal . ((r . B) - e)) * ((No_omega^ y1) .. B)) in L_ X1 ) by A17, A18, SURREALR:66;
hence ex b1, b2 being set st
( b1 in L_ X1 & b2 in L_ X1 & b1 <= x & x <= b2 ) ; :: thesis: verum
end;
A19: R_ X1 <==> R_ X2
proof
thus R_ X1 <=_ R_ X2 :: according to SURREALO:def 4 :: thesis: R_ X2 <=_ R_ X1
proof
let x be Surreal; :: according to SURREALO:def 3 :: thesis: ( not x in R_ X1 or ex b1, b2 being set st
( b1 in R_ X2 & b2 in R_ X2 & b1 <= x & x <= b2 ) )
assume x in R_ X1 ; :: thesis: ex b1, b2 being set st
( b1 in R_ X2 & b2 in R_ X2 & b1 <= x & x <= b2 )
then consider B being Element of A, e being positive Real such that
A20: ( x = (Sum ((r | B),((No_omega^ y1) | B))) + ((uReal . ((r . B) + e)) * ((No_omega^ y1) .. B)) & B in A ) ;
B c= O by A12, A20, ORDINAL1:10;
then A21: Sum ((r | B),((No_omega^ y1) | B)) = Sum ((r | B),((No_omega^ y2) | B)) by A11, A20;
(uReal . ((r . B) + e)) * ((No_omega^ y1) .. B) == (uReal . ((r . B) + e)) * ((No_omega^ y2) .. B) by A12, A20, A5, SURREALR:54;
then ( x == (Sum ((r | B),((No_omega^ y2) | B))) + ((uReal . ((r . B) + e)) * ((No_omega^ y2) .. B)) & (Sum ((r | B),((No_omega^ y2) | B))) + ((uReal . ((r . B) + e)) * ((No_omega^ y2) .. B)) in R_ X2 ) by A20, A21, SURREALR:66;
hence ex b1, b2 being set st
( b1 in R_ X2 & b2 in R_ X2 & b1 <= x & x <= b2 ) ; :: thesis: verum
end;
let x be Surreal; :: according to SURREALO:def 3 :: thesis: ( not x in R_ X2 or ex b1, b2 being set st
( b1 in R_ X1 & b2 in R_ X1 & b1 <= x & x <= b2 ) )
assume x in R_ X2 ; :: thesis: ex b1, b2 being set st
( b1 in R_ X1 & b2 in R_ X1 & b1 <= x & x <= b2 )
then consider B being Element of A, e being positive Real such that
A22: ( x = (Sum ((r | B),((No_omega^ y2) | B))) + ((uReal . ((r . B) + e)) * ((No_omega^ y2) .. B)) & B in A ) ;
B c= O by A12, A22, ORDINAL1:10;
then A23: Sum ((r | B),((No_omega^ y1) | B)) = Sum ((r | B),((No_omega^ y2) | B)) by A11, A22;
(uReal . ((r . B) + e)) * ((No_omega^ y1) .. B) == (uReal . ((r . B) + e)) * ((No_omega^ y2) .. B) by A12, A22, A5, SURREALR:54;
then ( x == (Sum ((r | B),((No_omega^ y1) | B))) + ((uReal . ((r . B) + e)) * ((No_omega^ y1) .. B)) & (Sum ((r | B),((No_omega^ y1) | B))) + ((uReal . ((r . B) + e)) * ((No_omega^ y1) .. B)) in R_ X1 ) by A22, A23, SURREALR:66;
hence ex b1, b2 being set st
( b1 in R_ X1 & b2 in R_ X1 & b1 <= x & x <= b2 ) ; :: thesis: verum
end;
A24: X1 == X2 by A14, A19, SURREALO:29;
A25: ( Sum ((r | A),((No_omega^ y1) | A)) = Unique_No X1 & Unique_No X1 == X1 ) by Th62, A13, A4, SURREALO:def 10;
A26: ( Sum ((r | A),((No_omega^ y2) | A)) = Unique_No X2 & Unique_No X2 == X2 ) by A2, Th62, A13, A4, SURREALO:def 10;
X2 == Sum ((r | A),((No_omega^ y1) | A)) by A24, A25, SURREALO:4;
then Sum ((r | A),((No_omega^ y2) | A)) == Sum ((r | A),((No_omega^ y1) | A)) by A26, SURREALO:4;
hence Sum ((r | A),((No_omega^ y1) | A)) = Sum ((r | A),((No_omega^ y2) | A)) by SURREALO:50; :: thesis: verum
end;
for A being Ordinal holds S1[A] from ORDINAL1:sch 2(A10);
 hence Sum ((r | O),((No_omega^ y1) | O)) = Sum ((r | O),((No_omega^ y2) | O)) ; :: thesis: verum