:: Surreal Numbers and Conway Names: A Formal Introduction to Their Interrelations
:: by Karol P\kak
::
:: Received September 6, 2026
:: Copyright (c) 2026 Association of Mizar Users

theorem Th1: :: SURREAL1:1

for f being Sequence holds f ^ {} = f

proof end;

theorem Th2: :: SURREAL1:2

for A being Ordinal
for f, g being Sequence st A c= dom f holds
(f ^ g) | A = f | A

proof end;

theorem Th3: :: SURREAL1:3

for A, B being Ordinal st A c= B holds
B = A +^ (B -^ A)

proof end;

theorem :: SURREAL1:4

for A being Ordinal
for f, g being Sequence st dom f c= A holds
(f ^ g) | A = f ^ (g | (A -^ (dom f)))

proof end;

theorem Th5: :: SURREAL1:5

for f, g1, g2 being Sequence st f ^ g1 = f ^ g2 holds
g1 = g2

proof end;

definition

let f be Sequence;
let A be Ordinal;

func f /^ A -> Sequence means :Def1: :: SURREAL1:def 1
( dom it = (dom f) -^ A & f = (f | A) ^ it );

existence
ex b₁ being Sequence st
( dom b₁ = (dom f) -^ A & f = (f | A) ^ b₁ )

proof end;

uniqueness
for b₁, b₂ being Sequence st dom b₁ = (dom f) -^ A & f = (f | A) ^ b₁ & dom b₂ = (dom f) -^ A & f = (f | A) ^ b₂ holds
b₁ = b₂ by Th5;

end;

:: deftheorem Def1 defines /^ SURREAL1:def 1 :
for f being Sequence
for A being Ordinal
for b₃ being Sequence holds
( b₃ = f /^ A iff ( dom b₃ = (dom f) -^ A & f = (f | A) ^ b₃ ) );

theorem Th6: :: SURREAL1:6

for A being Ordinal
for f being Sequence holds dom (f /^ A) c= dom f

proof end;

theorem Th7: :: SURREAL1:7

for A, B being Ordinal
for f being Sequence st A c= B holds
( f . B = (f /^ A) . (B -^ A) & ( B in dom f implies B -^ A in dom (f /^ A) ) & ( B -^ A in dom (f /^ A) implies B in dom f ) )

proof end;

theorem Th8: :: SURREAL1:8

for A, B being Ordinal
for f being Sequence holds
( f . (A +^ B) = (f /^ A) . B & ( A +^ B in dom f implies B in dom (f /^ A) ) & ( B in dom (f /^ A) implies A +^ B in dom f ) )

proof end;

registration

let D be set ;
let f be Sequence of D;
let A be Ordinal;

cluster f /^ A -> D -valued ;

coherence
f /^ A is D -valued

proof end;

end;

theorem Th9: :: SURREAL1:9

for A being Ordinal
for f being Sequence st succ A c= dom f holds
(f | (succ A)) /^ A = <%(f . A)%>

proof end;

theorem Th10: :: SURREAL1:10

for R being RelStr
for X being Subset of R holds
( X is well_founded iff subrelstr X is well_founded )

proof end;

theorem Th11: :: SURREAL1:11

for R being RelStr holds {} R is well_founded

proof end;

theorem Th12: :: SURREAL1:12

for R being non empty RelStr
for X being Subset of R holds
( X is well_founded iff for f being sequence of R holds
( not rng f c= X or not f is descending ) )

proof end;

theorem Th13: :: SURREAL1:13

for R being non empty transitive antisymmetric RelStr
for f being sequence of R st f is descending holds
for s being subsequence of f holds s is descending

proof end;

registration

let R be non empty transitive antisymmetric RelStr ;

cluster Function-like quasi_total descending -> one-to-one for Element of bool [:omega, the carrier of R:];

coherence
for b₁ being sequence of R st b₁ is descending holds
b₁ is one-to-one

proof end;

end;

theorem Th14: :: SURREAL1:14

for R being non empty RelStr
for f being sequence of R
for X being Subset of R st X /\ (rng f) is infinite holds
ex s being subsequence of f st rng s c= X

proof end;

theorem Th15: :: SURREAL1:15

for R being RelStr
for X, Y being Subset of R st X c= Y & Y is well_founded holds
X is well_founded

proof end;

theorem Th16: :: SURREAL1:16

for R being transitive antisymmetric RelStr
for X being Subset of R st X is finite holds
X is well_founded

proof end;

theorem Th17: :: SURREAL1:17

for R being transitive antisymmetric RelStr
for X, Y being well_founded Subset of R holds X \/ Y is well_founded

proof end;

definition

let R be non empty RelStr ;
let s be sequence of R;

attr s is non-descending means :: SURREAL1:def 2
for n being Nat holds [(s . n),(s . (n + 1))] in the InternalRel of R;

end;

:: deftheorem defines non-descending SURREAL1:def 2 :
for R being non empty RelStr
for s being sequence of R holds
( s is non-descending iff for n being Nat holds [(s . n),(s . (n + 1))] in the InternalRel of R );

theorem Th18: :: SURREAL1:18

for R being non empty transitive RelStr
for f being sequence of R st f is non-descending holds
for i, j being Nat st i < j holds
[(f . i),(f . j)] in the InternalRel of R

proof end;

theorem Th19: :: SURREAL1:19

for R being non empty reflexive RelStr
for f being sequence of R st R is connected holds
for X being Subset of R st rng f c= X & X is well_founded holds
ex s being subsequence of f st s is non-descending

proof end;

theorem Th20: :: SURREAL1:20

for R being non empty transitive RelStr
for f being sequence of R st f is non-descending holds
for s being subsequence of f holds s is non-descending

proof end;

definition

let R be Relation;
let s be Sequence of field R;

attr s is increasing means :: SURREAL1:def 3
for A, B being Ordinal st A in B & B in dom s holds
( s . A <> s . B & [(s . A),(s . B)] in R );

end;

:: deftheorem defines increasing SURREAL1:def 3 :
for R being Relation
for s being Sequence of field R holds
( s is increasing iff for A, B being Ordinal st A in B & B in dom s holds
( s . A <> s . B & [(s . A),(s . B)] in R ) );

registration

let R be Relation;

cluster Relation-like field R -valued Function-like Sequence-like increasing -> one-to-one for set ;

coherence
for b₁ being Sequence of field R st b₁ is increasing holds
b₁ is one-to-one

proof end;

end;

theorem Th21: :: SURREAL1:21

for R being Relation
for X being set st X = field (R |_2 X) holds
( ( R |_2 X is reflexive implies R is_reflexive_in X ) & ( R |_2 X is connected implies R is_connected_in X ) & ( R |_2 X is well_founded implies R is_well_founded_in X ) )

proof end;

theorem Th22: :: SURREAL1:22

for R being Relation
for X being set holds
( ( R |_2 X is transitive implies R is_transitive_in X ) & ( R |_2 X is antisymmetric implies R is_antisymmetric_in X ) )

proof end;

theorem Th23: :: SURREAL1:23

for R being Relation
for X being Subset of (field R) st R |_2 X is_reflexive_in X & R |_2 X is_antisymmetric_in X holds
for s being Sequence of field R st rng s = X & s is increasing holds
s is_isomorphism_of RelIncl (dom s),R |_2 X

proof end;

theorem Th24: :: SURREAL1:24

for R being Relation
for X being Subset of (field R) holds
( R well_orders X iff ( R |_2 X is_reflexive_in X & R |_2 X is_antisymmetric_in X & ex s being Sequence of field R st
( rng s = X & s is increasing ) ) )

proof end;

theorem Th25: :: SURREAL1:25

for R being Relation
for X being Subset of (field R) st R |_2 X is_reflexive_in X & R |_2 X is_antisymmetric_in X holds
for s, t being Sequence of field R st rng s = X & X = rng t & s is increasing & t is increasing holds
s = t

proof end;

definition

let R be RelStr ;
let A be Subset of R;

attr A is well-ordering means :: SURREAL1:def 4
the InternalRel of R well_orders A;

end;

:: deftheorem defines well-ordering SURREAL1:def 4 :
for R being RelStr
for A being Subset of R holds
( A is well-ordering iff the InternalRel of R well_orders A );

registration

let R be RelStr ;

cluster {} R -> well-ordering ;

coherence
{} R is well-ordering

proof end;

end;

theorem Th26: :: SURREAL1:26

for R being RelStr
for X, Y being Subset of R st X c= Y & Y is well-ordering holds
X is well-ordering

proof end;

theorem Th27: :: SURREAL1:27

for A being Ordinal
for X being Subset of A ex s being Ordinal-Sequence st
( s is increasing & rng s = X )

proof end;

theorem Th28: :: SURREAL1:28

for x1, x2, y1, y2 being Surreal st x1 == x2 & y1 == y2 holds
x1 - y1 == x2 - y2

proof end;

theorem Th29: :: SURREAL1:29

for x1, x2, y1, y2 being Surreal st x1 == x2 & y1 == y2 holds
x1 * y1 == x2 * y2

proof end;

Lm1: for s, z being Surreal
for r, e being Real holds s + ((uReal . (r + e)) * z) == (s + ((uReal . r) * z)) + ((uReal . e) * z)

proof end;

theorem Th30: :: SURREAL1:30

for s, z being Surreal
for r, e being Real holds
( s + ((uReal . (r + e)) * z) == (s + ((uReal . r) * z)) + ((uReal . e) * z) & s + ((uReal . (r - e)) * z) == (s + ((uReal . r) * z)) - ((uReal . e) * z) )

proof end;

Lm2: for x being Surreal holds - x <= |.x.|

proof end;

theorem Th31: :: SURREAL1:31

for x, y being Surreal
for r being Real st 0_No <= x & x infinitely< y holds
|.((uReal . r) * x).| infinitely< y

proof end;

theorem Th32: :: SURREAL1:32

for r1, r2 being Real holds (uReal . r1) - (uReal . r2) == uReal . (r1 - r2)

proof end;

theorem Th33: :: SURREAL1:33

for x being Surreal
for r being Real holds x * (uReal . r) == - (x * (uReal . (- r)))

proof end;

theorem Th34: :: SURREAL1:34

for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds
X1 ++ Y1 c= X2 ++ Y2

proof end;

definition

let o be object ;
let f be surreal-valued Function;
assume A1: o in dom f ;

func f .. o -> Surreal equals :Def5: :: SURREAL1:def 5
f . o;

coherence
f . o is Surreal

proof end;

end;

:: deftheorem Def5 defines .. SURREAL1:def 5 :
for o being object
for f being surreal-valued Function st o in dom f holds
f .. o = f . o;

definition

let S be Surreal-Sequence;

redefine attr S is positive means :Def6: :: SURREAL1:def 6
for A being Ordinal st A in dom S holds
S .. A is positive ;

compatibility
( S is positive iff for A being Ordinal st A in dom S holds
S .. A is positive )

proof end;

end;

:: deftheorem Def6 defines positive SURREAL1:def 6 :
for S being Surreal-Sequence holds
( S is positive iff for A being Ordinal st A in dom S holds
S .. A is positive );

definition

let S be Surreal-Sequence;

redefine attr S is decreasing_infinitely means :Def7: :: SURREAL1:def 7
for A, B being Ordinal st A in B & B in dom S holds
S .. B infinitely< S .. A;

compatibility
( S is decreasing_infinitely iff for A, B being Ordinal st A in B & B in dom S holds
S .. B infinitely< S .. A )

proof end;

end;

:: deftheorem Def7 defines decreasing_infinitely SURREAL1:def 7 :
for S being Surreal-Sequence holds
( S is decreasing_infinitely iff for A, B being Ordinal st A in B & B in dom S holds
S .. B infinitely< S .. A );

registration

cluster Relation-like Function-like Sequence-like surreal-valued decreasing_infinitely -> one-to-one for set ;

coherence
for b₁ being Surreal-Sequence st b₁ is decreasing_infinitely holds
b₁ is one-to-one

proof end;

end;

registration

let f be Surreal-Sequence;
let A be Ordinal;

cluster f /^ A -> surreal-valued ;

coherence
f /^ A is surreal-valued

proof end;

end;

theorem Th35: :: SURREAL1:35

for A, B being Ordinal
for f being Surreal-Sequence st A c= B & B in dom f holds
f .. B = (f /^ A) .. (B -^ A)

proof end;

theorem Th36: :: SURREAL1:36

for A, B being Ordinal
for f being Surreal-Sequence st ( A +^ B in dom f or B in dom (f /^ A) ) holds
f .. (A +^ B) = (f /^ A) .. B

proof end;

registration

let f be positive Surreal-Sequence;
let A be Ordinal;

cluster f /^ A -> positive ;

coherence
f /^ A is positive

proof end;

end;

registration

let f be decreasing_infinitely Surreal-Sequence;
let A be Ordinal;

cluster f /^ A -> decreasing_infinitely ;

coherence
f /^ A is decreasing_infinitely

proof end;

end;

definition

let S be surreal-membered set ;

func Unique_No S -> uniq-surreal-membered set means :Def8: :: SURREAL1:def 8
for x being Surreal holds
( x in it iff ex y being Surreal st
( y in S & x = Unique_No y ) );

existence
ex b₁ being uniq-surreal-membered set st
for x being Surreal holds
( x in b₁ iff ex y being Surreal st
( y in S & x = Unique_No y ) )

proof end;

uniqueness
for b₁, b₂ being uniq-surreal-membered set st ( for x being Surreal holds
( x in b₁ iff ex y being Surreal st
( y in S & x = Unique_No y ) ) ) & ( for x being Surreal holds
( x in b₂ iff ex y being Surreal st
( y in S & x = Unique_No y ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines Unique_No SURREAL1:def 8 :
for S being surreal-membered set
for b₂ being uniq-surreal-membered set holds
( b₂ = Unique_No S iff for x being Surreal holds
( x in b₂ iff ex y being Surreal st
( y in S & x = Unique_No y ) ) );

definition

let s be Surreal-Sequence;

func Unique_No s -> uSurreal-Sequence means :Def9: :: SURREAL1:def 9
( dom it = dom s & ( for A being Ordinal st A in dom s holds
it . A = Unique_No (s .. A) ) );

existence
ex b₁ being uSurreal-Sequence st
( dom b₁ = dom s & ( for A being Ordinal st A in dom s holds
b₁ . A = Unique_No (s .. A) ) )

proof end;

uniqueness
for b₁, b₂ being uSurreal-Sequence st dom b₁ = dom s & ( for A being Ordinal st A in dom s holds
b₁ . A = Unique_No (s .. A) ) & dom b₂ = dom s & ( for A being Ordinal st A in dom s holds
b₂ . A = Unique_No (s .. A) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines Unique_No SURREAL1:def 9 :
for s being Surreal-Sequence
for b₂ being uSurreal-Sequence holds
( b₂ = Unique_No s iff ( dom b₂ = dom s & ( for A being Ordinal st A in dom s holds
b₂ . A = Unique_No (s .. A) ) ) );

theorem Th37: :: SURREAL1:37

for s being Surreal-Sequence holds Unique_No (rng s) = rng (Unique_No s)

proof end;

theorem Th38: :: SURREAL1:38

for S, T being surreal-membered set holds Unique_No (S ++ T) = Unique_No ((Unique_No S) ++ (Unique_No T))

proof end;

theorem Th39: :: SURREAL1:39

for S being surreal-membered set holds
( Unique_No S = {} iff S = {} )

proof end;

definition

let X be surreal-membered set ;

func RevSurrStr X -> strict RelStr means :Def10: :: SURREAL1:def 10
( the carrier of it = X & ( for a, b being Surreal st a in X & b in X holds
( a <= b iff [b,a] in the InternalRel of it ) ) );

existence
ex b₁ being strict RelStr st
( the carrier of b₁ = X & ( for a, b being Surreal st a in X & b in X holds
( a <= b iff [b,a] in the InternalRel of b₁ ) ) )

proof end;

uniqueness
for b₁, b₂ being strict RelStr st the carrier of b₁ = X & ( for a, b being Surreal st a in X & b in X holds
( a <= b iff [b,a] in the InternalRel of b₁ ) ) & the carrier of b₂ = X & ( for a, b being Surreal st a in X & b in X holds
( a <= b iff [b,a] in the InternalRel of b₂ ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines RevSurrStr SURREAL1:def 10 :
for X being surreal-membered set
for b₂ being strict RelStr holds
( b₂ = RevSurrStr X iff ( the carrier of b₂ = X & ( for a, b being Surreal st a in X & b in X holds
( a <= b iff [b,a] in the InternalRel of b₂ ) ) ) );

registration

let X be surreal-membered set ;

cluster RevSurrStr X -> strict reflexive transitive ;

coherence
( RevSurrStr X is reflexive & RevSurrStr X is transitive )

proof end;

end;

registration

let X be non empty surreal-membered set ;

cluster RevSurrStr X -> non empty strict ;

coherence
not RevSurrStr X is empty by Def10;

end;

registration

let X be non empty surreal-membered set ;

cluster RevSurrStr X -> strict connected ;

coherence
RevSurrStr X is connected

proof end;

end;

definition

let X be surreal-membered set ;

attr X is ==_distinct means :Def11: :: SURREAL1:def 11
for x1, x2 being Surreal st x1 in X & x2 in X & x1 == x2 holds
x1 = x2;

end;

:: deftheorem Def11 defines ==_distinct SURREAL1:def 11 :
for X being surreal-membered set holds
( X is ==_distinct iff for x1, x2 being Surreal st x1 in X & x2 in X & x1 == x2 holds
x1 = x2 );

registration

cluster uniq-surreal-membered -> uniq-surreal-membered ==_distinct for set ;

coherence
for b₁ being uniq-surreal-membered set holds b₁ is ==_distinct

proof end;

end;

registration

cluster non empty surreal-membered ==_distinct for set ;

existence
ex b₁ being surreal-membered set st
( not b₁ is empty & b₁ is ==_distinct )

proof end;

end;

registration

let S be surreal-membered ==_distinct set ;

cluster RevSurrStr S -> strict antisymmetric ;

coherence
RevSurrStr S is antisymmetric

proof end;

end;

definition

let S be surreal-membered set ;

attr S is desc_ordering means :Def12: :: SURREAL1:def 12
ex y being strictly_decreasing Surreal-Sequence st rng y = S;

end;

:: deftheorem Def12 defines desc_ordering SURREAL1:def 12 :
for S being surreal-membered set holds
( S is desc_ordering iff ex y being strictly_decreasing Surreal-Sequence st rng y = S );

registration

cluster surreal-membered desc_ordering -> surreal-membered ==_distinct for set ;

coherence
for b₁ being surreal-membered set st b₁ is desc_ordering holds
b₁ is ==_distinct

proof end;

end;

registration

let S be surreal-membered ==_distinct set ;

cluster -> ==_distinct for Element of bool S;

coherence
for b₁ being Subset of S holds b₁ is ==_distinct by Def11;

end;

theorem Th40: :: SURREAL1:40

for S being surreal-membered set
for A being Subset of S holds field ( the InternalRel of (RevSurrStr S) |_2 A) = A

proof end;

registration

let S be surreal-membered set ;

cluster -> surreal-membered for Element of bool the carrier of (RevSurrStr S);

coherence
for b₁ being Subset of (RevSurrStr S) holds b₁ is surreal-membered

proof end;

end;

theorem Th41: :: SURREAL1:41

for S being surreal-membered set holds field the InternalRel of (RevSurrStr S) = S

proof end;

theorem Th42: :: SURREAL1:42

for s being Surreal-Sequence
for X being surreal-membered ==_distinct set st rng s c= X holds
( s is Sequence of field the InternalRel of (RevSurrStr X) & ( for t being Sequence of field the InternalRel of (RevSurrStr X) st t = s holds
( s is strictly_decreasing iff t is increasing ) ) )

proof end;

:: Characterization of Well-Ordering via Strictly Descending Sequences

theorem Th43: :: SURREAL1:43

for S being surreal-membered ==_distinct set
for A being Subset of (RevSurrStr S) holds
( A is desc_ordering iff A is well-ordering )

proof end;

registration

let s be strictly_decreasing Surreal-Sequence;

cluster rng s -> desc_ordering ;

coherence
rng s is desc_ordering ;

end;

registration

cluster non empty surreal-membered uniq-surreal-membered ==_distinct desc_ordering for set ;

existence
ex b₁ being uniq-surreal-membered set st
( not b₁ is empty & b₁ is desc_ordering )

proof end;

end;

registration

cluster {} -> desc_ordering ;

coherence
{} is desc_ordering

proof end;

end;

theorem Th44: :: SURREAL1:44

for S being surreal-membered ==_distinct set
for A being Subset of (RevSurrStr S) st A is well_founded holds
A is well-ordering

proof end;

registration

let S be surreal-membered desc_ordering set ;

cluster -> desc_ordering for Element of bool S;

coherence
for b₁ being Subset of S holds b₁ is desc_ordering

proof end;

end;

registration

let S be surreal-membered ==_distinct set ;

cluster finite -> desc_ordering for Element of bool S;

coherence
for b₁ being Subset of S st b₁ is finite holds
b₁ is desc_ordering

proof end;

end;

registration

let S be surreal-membered ==_distinct set ;

cluster finite surreal-membered ==_distinct desc_ordering for Element of bool S;

existence
ex b₁ being Subset of S st
( b₁ is finite & b₁ is desc_ordering )

proof end;

end;

:: Union of Descending Orderings

registration

let S be surreal-membered ==_distinct set ;
let A, B be desc_ordering Subset of S;

cluster A \/ B -> desc_ordering ;

coherence
A \/ B is desc_ordering

proof end;

end;

theorem Th45: :: SURREAL1:45

for s being Surreal-Sequence holds
( s is strictly_decreasing iff Unique_No s is strictly_decreasing )

proof end;

registration

let z be strictly_decreasing Surreal-Sequence;

cluster Unique_No z -> strictly_decreasing ;

coherence
Unique_No z is strictly_decreasing by Th45;

end;

theorem Th46: :: SURREAL1:46

for S being surreal-membered desc_ordering set holds Unique_No S is desc_ordering

proof end;

:: Closure of Descending Orderings under Addition

theorem Th47: :: SURREAL1:47

for S, T being surreal-membered desc_ordering set holds Unique_No (S ++ T) is desc_ordering

proof end;

theorem Th48: :: SURREAL1:48

for S, T being surreal-membered set st S c= T holds
Unique_No S c= Unique_No T

proof end;

definition

let S be surreal-membered set ;
assume A1: S is desc_ordering ;

func ord S -> strictly_decreasing Surreal-Sequence means :Def13: :: SURREAL1:def 13
rng it = S;

existence
ex b₁ being strictly_decreasing Surreal-Sequence st rng b₁ = S by A1;
uniqueness
for b₁, b₂ being strictly_decreasing Surreal-Sequence st rng b₁ = S & rng b₂ = S holds
b₁ = b₂

proof end;

end;

:: deftheorem Def13 defines ord SURREAL1:def 13 :
for S being surreal-membered set st S is desc_ordering holds
for b₂ being strictly_decreasing Surreal-Sequence holds
( b₂ = ord S iff rng b₂ = S );

registration

cluster Relation-like Function-like Sequence-like surreal-valued strictly_decreasing -> one-to-one for set ;

coherence
for b₁ being Surreal-Sequence st b₁ is strictly_decreasing holds
b₁ is one-to-one

proof end;

end;

theorem Th49: :: SURREAL1:49

for r being Real holds [ { (uReal . (r - e1)) where e1 is positive Real : verum } , { (uReal . (r + e2)) where e2 is positive Real : verum } ] is Surreal

proof end;

theorem Th50: :: SURREAL1:50

for r being Real holds [ { (uReal . (r - e1)) where e1 is positive Real : r - e1 > 0 } , { (uReal . (r + e2)) where e2 is positive Real : verum } ] is Surreal

proof end;

theorem Th51: :: SURREAL1:51

for r being Real
for z being Surreal st z > 0_No holds
[ { ((uReal . (r - e1)) * z) where e1 is positive Real : verum } , { ((uReal . (r + e2)) * z) where e2 is positive Real : verum } ] is Surreal

proof end;

theorem Th52: :: SURREAL1:52

for s, z being Surreal
for r being Real st z > 0_No holds
[ { (s + ((uReal . (r - e1)) * z)) where e1 is positive Real : verum } , { (s + ((uReal . (r + e2)) * z)) where e2 is positive Real : verum } ] is Surreal

proof end;

theorem Th53: :: SURREAL1:53

for x, y being Surreal st L_ x << {y} & {y} << R_ x holds
( born (Unique_No x) c= born y & ( not x == y implies born (Unique_No x) in born y ) )

proof end;

theorem Th54: :: SURREAL1:54

for s, z, x being Surreal
for r being Real st x = [ { (s + ((uReal . (r - e1)) * z)) where e1 is positive Real : verum } , { (s + ((uReal . (r + e2)) * z)) where e2 is positive Real : verum } ] holds
( x is s,z,r _Term & ( for u1, u2 being uSurreal st u1 == x & u1 <> u2 & u2 is s,z,r _Term holds
born u1 in born u2 ) )

proof end;

theorem Th55: :: SURREAL1:55

for r being positive Real
for x being Surreal st x = [ { (uReal . (r - e1)) where e1 is positive Real : r - e1 > 0 } , { (uReal . (r + e2)) where e2 is positive Real : verum } ] holds
x == uReal . r

proof end;

theorem Th56: :: SURREAL1:56

for r being Real
for x being Surreal st x = [ { (uReal . (r - e1)) where e1 is positive Real : verum } , { (uReal . (r + e2)) where e2 is positive Real : verum } ] holds
x == uReal . r

proof end;

:: Gonshor'86 Lemma 5.2

theorem Th57: :: SURREAL1:57

for r being Real
for z, x being Surreal st x = [ { ((uReal . (r - e1)) * (No_omega^ z)) where e1 is positive Real : verum } , { ((uReal . (r + e2)) * (No_omega^ z)) where e2 is positive Real : verum } ] holds
(uReal . r) * (No_omega^ z) == x

proof end;

theorem Th58: :: SURREAL1:58

for A being Ordinal
for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence st A c= (dom r) /\ (dom y) holds
(Partial_Sums (r,y)) . A = Sum ((r | A),(y | A))

proof end;

theorem Th59: :: SURREAL1:59

for A being Ordinal
for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence st succ A c= (dom r) /\ (dom y) holds
[ { ((Sum ((r | A),(y | A))) + ((uReal . ((r . A) - e1)) * (y .. A))) where e1 is positive Real : verum } , { ((Sum ((r | A),(y | A))) + ((uReal . ((r . A) + e2)) * (y .. A))) where e2 is positive Real : verum } ] is Surreal

proof end;

theorem Th60: :: SURREAL1:60

for A being Ordinal
for x being Surreal
for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence st succ A c= (dom r) /\ (dom y) & x = [ { ((Sum ((r | A),(y | A))) + ((uReal . ((r . A) - e1)) * (y .. A))) where e1 is positive Real : verum } , { ((Sum ((r | A),(y | A))) + ((uReal . ((r . A) + e2)) * (y .. A))) where e2 is positive Real : verum } ] holds
Sum ((r | (succ A)),(y | (succ A))) = Unique_No x

proof end;

Lm3: for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence
for A being Ordinal st A c= (dom r) /\ (dom y) holds
for Sl, Sr being set st Sl = { ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) - e1)) * (y .. B))) where B is Element of A, e1 is positive Real : B in A } & Sr = { ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) + e2)) * (y .. B))) where B is Element of A, e2 is positive Real : B in A } holds
( Sl is surreal-membered & Sr is surreal-membered & Sl << {(Sum ((r | A),(y | A)))} & {(Sum ((r | A),(y | A)))} << Sr )

proof end;

theorem Th61: :: SURREAL1:61

for A being Ordinal
for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence st A c= (dom r) /\ (dom y) holds
[ { ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) - e)) * (y .. B))) where B is Element of A, e is positive Real : B in A } , { ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) + e)) * (y .. B))) where B is Element of A, e is positive Real : B in A } ] is Surreal

proof end;

:: Gonshor'86 Lemma 5.3

theorem Th62: :: SURREAL1:62

for A being Ordinal
for x being Surreal
for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence st A c= (dom r) /\ (dom y) & x = [ { ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) - e)) * (y .. B))) where B is Element of A, e is positive Real : B in A } , { ((Sum ((r | B),(y | B))) + ((uReal . ((r . B) + e)) * (y .. B))) where B is Element of A, e is positive Real : B in A } ] holds
Sum ((r | A),(y | A)) = Unique_No x

proof end;

theorem Th63: :: SURREAL1:63

for A being Ordinal
for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence st succ A c= (dom r) /\ (dom y) & ( for ry being Surreal st ry = [ { ((uReal . ((r . A) - e1)) * (y .. A)) where e1 is positive Real : verum } , { ((uReal . ((r . A) + e2)) * (y .. A)) where e2 is positive Real : verum } ] holds
ry == (uReal . (r . A)) * (y .. A) ) holds
Sum ((r | (succ A)),(y | (succ A))) == (Sum ((r | A),(y | A))) + ((uReal . (r . A)) * (y .. A))

proof end;

theorem Th64: :: SURREAL1:64

for A being Ordinal
for r being Sequence of REAL
for y being strictly_decreasing Surreal-Sequence st succ A c= (dom r) /\ (dom y) holds
Sum ((r | (succ A)),(No_omega^ (y | (succ A)))) == (Sum ((r | A),(No_omega^ (y | A)))) + ((uReal . (r . A)) * (No_omega^ (y .. A)))

proof end;

theorem :: SURREAL1:65

for A being Ordinal
for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence st A in (dom r) /\ (dom y) & r . A = 0 holds
Sum ((r | A),(y | A)) = Sum ((r | (succ A)),(y | (succ A)))

proof end;

theorem Th66: :: SURREAL1:66

for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence st rng r c= {0} holds
Sum (r,y) = 0_No

proof end;

theorem Th67: :: SURREAL1:67

for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence holds Sum ((r | 0),(y | 0)) = 0_No

proof end;

theorem Th68: :: SURREAL1:68

for A, B being Ordinal
for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence st B in A & A c= (dom r) /\ (dom y) holds
Sum ((r | A),(y | A)) is Sum ((r | B),(y | B)),y .. B,r . B _Term

proof end;

theorem Th69: :: SURREAL1:69

for A, B being Ordinal
for e being positive Real
for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence st B in A & A c= (dom r) /\ (dom y) holds
( (Sum ((r | B),(y | B))) + ((uReal . ((r . B) - e)) * (y .. B)) < Sum ((r | A),(y | A)) & Sum ((r | A),(y | A)) < (Sum ((r | B),(y | B))) + ((uReal . ((r . B) + e)) * (y .. B)) )

proof end;

theorem Th70: :: SURREAL1:70

for a being Surreal
for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence st 0 in (dom y) /\ (dom r) & y .. 0 infinitely< a holds
|.(Sum (r,y)).| infinitely< a

proof end;

:: Gonshor'86 Lemma 5.5
:: Decomposition of Selected Surreal Representations into Head and Tail

theorem Th71: :: SURREAL1:71

for A being Ordinal
for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence st A c= (dom r) /\ (dom y) holds
(Sum ((r | A),(y | A))) + (Sum ((r /^ A),(y /^ A))) == Sum (r,y)

proof end;

theorem Th72: :: SURREAL1:72

for A, B being Ordinal
for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence st A c= B & B c= (dom r) /\ (dom y) & ( for C being Ordinal st A c= C & C in B holds
r . C = 0 ) holds
Sum ((r | B),(y | B)) = Sum ((r | A),(y | A))

proof end;

::Gonshor'86 Lemma5.4
:: Invariance of Surreal Sums under Zero Coefficient Extension

theorem Th73: :: SURREAL1:73

for r, rE being Sequence of REAL
for y, yE being positive decreasing_infinitely Surreal-Sequence st dom r = dom y & dom rE = dom yE & rng y c= rng yE & ( for A, B being Ordinal st A in dom y & B in dom yE & y . A = yE . B holds
r . A = rE . B ) & ( for A being Ordinal st A in dom yE & not yE . A in rng y holds
rE . A = 0 ) holds
Sum (r,y) = Sum (rE,yE)

proof end;

:: The Additive Law for Compatible Selected Surreal Series

theorem Th74: :: SURREAL1:74

for A being Ordinal
for y being positive decreasing_infinitely Surreal-Sequence
for r, s being Sequence of REAL st dom r = dom s & A c= (dom r) /\ (dom y) holds
Sum (((r + s) | A),(y | A)) == (Sum ((r | A),(y | A))) + (Sum ((s | A),(y | A)))

proof end;

theorem Th75: :: SURREAL1:75

for A being Ordinal
for y being positive decreasing_infinitely Surreal-Sequence
for r being Sequence of REAL st A c= (dom r) /\ (dom y) holds
Sum (((- r) | A),(y | A)) == - (Sum ((r | A),(y | A)))

proof end;

definition

let r be Sequence of REAL ;
let y be one-to-one Sequence;
let yE be Sequence;

func r -extended_by (y,yE) -> Sequence of REAL means :Def14: :: SURREAL1:def 14
( dom it = dom yE & ( for A, B being Ordinal st A in dom y & B in dom yE & y . A = yE . B holds
r . A = it . B ) & ( for A being Ordinal st A in dom yE & not yE . A in rng y holds
it . A = 0 ) );

existence
ex b₁ being Sequence of REAL st
( dom b₁ = dom yE & ( for A, B being Ordinal st A in dom y & B in dom yE & y . A = yE . B holds
r . A = b₁ . B ) & ( for A being Ordinal st A in dom yE & not yE . A in rng y holds
b₁ . A = 0 ) )

proof end;

uniqueness
for b₁, b₂ being Sequence of REAL st dom b₁ = dom yE & ( for A, B being Ordinal st A in dom y & B in dom yE & y . A = yE . B holds
r . A = b₁ . B ) & ( for A being Ordinal st A in dom yE & not yE . A in rng y holds
b₁ . A = 0 ) & dom b₂ = dom yE & ( for A, B being Ordinal st A in dom y & B in dom yE & y . A = yE . B holds
r . A = b₂ . B ) & ( for A being Ordinal st A in dom yE & not yE . A in rng y holds
b₂ . A = 0 ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def14 defines -extended_by SURREAL1:def 14 :
for r being Sequence of REAL
for y being one-to-one Sequence
for yE being Sequence
for b₄ being Sequence of REAL holds
( b₄ = r -extended_by (y,yE) iff ( dom b₄ = dom yE & ( for A, B being Ordinal st A in dom y & B in dom yE & y . A = yE . B holds
r . A = b₄ . B ) & ( for A being Ordinal st A in dom yE & not yE . A in rng y holds
b₄ . A = 0 ) ) );

theorem Th76: :: SURREAL1:76

for r being Sequence of REAL
for y, yE being strictly_decreasing Surreal-Sequence st rng (y | (dom r)) c= rng yE & rng yE is ==_distinct holds
Sum (r,(No_omega^ y)) = Sum ((r -extended_by ((y | (dom r)),yE)),(No_omega^ yE))

proof end;

definition

let A, B be Ordinal;
let r, s be Sequence of REAL ;

func Product (r,s,A,B) -> Function of [:A,B:],REAL means :Def15: :: SURREAL1:def 15
for a, b being Ordinal st a in A & b in B holds
it . (a,b) = (r . a) * (s . b);

existence
ex b₁ being Function of [:A,B:],REAL st
for a, b being Ordinal st a in A & b in B holds
b₁ . (a,b) = (r . a) * (s . b)

proof end;

uniqueness
for b₁, b₂ being Function of [:A,B:],REAL st ( for a, b being Ordinal st a in A & b in B holds
b₁ . (a,b) = (r . a) * (s . b) ) & ( for a, b being Ordinal st a in A & b in B holds
b₂ . (a,b) = (r . a) * (s . b) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def15 defines Product SURREAL1:def 15 :
for A, B being Ordinal
for r, s being Sequence of REAL
for b₅ being Function of [:A,B:],REAL holds
( b₅ = Product (r,s,A,B) iff for a, b being Ordinal st a in A & b in B holds
b₅ . (a,b) = (r . a) * (s . b) );

definition

let A, B be Ordinal;
let y, z be strictly_decreasing Surreal-Sequence;
assume A1: ( dom y c= A & dom z c= B ) ;
let s be Surreal;

func (y,z,A,B) += s -> Element of Fin [:A,B:] means :Def16: :: SURREAL1:def 16
for a, b being Ordinal holds
( [a,b] in it iff ( a in dom y & b in dom z & (y .. a) + (z .. b) == s ) );

existence
ex b₁ being Element of Fin [:A,B:] st
for a, b being Ordinal holds
( [a,b] in b₁ iff ( a in dom y & b in dom z & (y .. a) + (z .. b) == s ) )

proof end;

uniqueness
for b₁, b₂ being Element of Fin [:A,B:] st ( for a, b being Ordinal holds
( [a,b] in b₁ iff ( a in dom y & b in dom z & (y .. a) + (z .. b) == s ) ) ) & ( for a, b being Ordinal holds
( [a,b] in b₂ iff ( a in dom y & b in dom z & (y .. a) + (z .. b) == s ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def16 defines += SURREAL1:def 16 :
for A, B being Ordinal
for y, z being strictly_decreasing Surreal-Sequence st dom y c= A & dom z c= B holds
for s being Surreal
for b₆ being Element of Fin [:A,B:] holds
( b₆ = (y,z,A,B) += s iff for a, b being Ordinal holds
( [a,b] in b₆ iff ( a in dom y & b in dom z & (y .. a) + (z .. b) == s ) ) );

theorem Th77: :: SURREAL1:77

for A, B being Ordinal
for a, b being Surreal
for y, z being strictly_decreasing Surreal-Sequence st dom y c= A & dom z c= B & a == b holds
(y,z,A,B) += a c= (y,z,A,B) += b

proof end;

theorem Th78: :: SURREAL1:78

for A, B being Ordinal
for y, z being strictly_decreasing Surreal-Sequence
for c being Surreal st dom y c= A & dom z c= B & ( for a being Surreal st a == c holds
not a in (rng y) ++ (rng z) ) holds
(y,z,A,B) += c = {}

proof end;

Lm4: for x, y being Surreal
for a, b, c, d, e being Real holds ((uReal . (a - b)) * (x + ((uReal . (c + d)) * y))) + ((uReal . b) * (x + ((uReal . (c - e)) * y))) == ((uReal . a) * x) + ((uReal . (((a * c) - (b * e)) + (d * (a - b)))) * y)

proof end;

Lm5: for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence
for x being positive Real
for A being Ordinal st A c= (dom r) /\ (dom y) holds
Sum (((x (#) r) | A),(y | A)) == (uReal . x) * (Sum ((r | A),(y | A)))

proof end;

theorem Th79: :: SURREAL1:79

for A being Ordinal
for r being Sequence of REAL
for y being positive decreasing_infinitely Surreal-Sequence
for x being Real st A c= (dom r) /\ (dom y) holds
Sum (((x (#) r) | A),(y | A)) == (uReal . x) * (Sum ((r | A),(y | A)))

proof end;

definition

let s be Surreal-Sequence;
let a be Surreal;

func s + a -> Surreal-Sequence means :Def17: :: SURREAL1:def 17
( dom it = dom s & ( for A being Ordinal st A in dom s holds
it . A = (s .. A) + a ) );

existence
ex b₁ being Surreal-Sequence st
( dom b₁ = dom s & ( for A being Ordinal st A in dom s holds
b₁ . A = (s .. A) + a ) )

proof end;

uniqueness
for b₁, b₂ being Surreal-Sequence st dom b₁ = dom s & ( for A being Ordinal st A in dom s holds
b₁ . A = (s .. A) + a ) & dom b₂ = dom s & ( for A being Ordinal st A in dom s holds
b₂ . A = (s .. A) + a ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def17 defines + SURREAL1:def 17 :
for s being Surreal-Sequence
for a being Surreal
for b₃ being Surreal-Sequence holds
( b₃ = s + a iff ( dom b₃ = dom s & ( for A being Ordinal st A in dom s holds
b₃ . A = (s .. A) + a ) ) );

registration

let s be strictly_decreasing Surreal-Sequence;
let a be Surreal;

cluster s + a -> strictly_decreasing ;

coherence
s + a is strictly_decreasing

proof end;

end;

theorem :: SURREAL1:80

for A being Ordinal
for x being Surreal
for s being Surreal-Sequence holds (s | A) + x = (s + x) | A

proof end;

theorem Th81: :: SURREAL1:81

for a being Surreal
for y being strictly_decreasing Surreal-Sequence holds rng (y + a) = (rng y) ++ {a}

proof end;

theorem Th82: :: SURREAL1:82

for A being Ordinal
for a being Surreal
for s being Surreal-Sequence st A in dom s holds
(No_omega^ a) * ((No_omega^ s) .. A) == (No_omega^ (s + a)) .. A

proof end;

Lm6: for a, b, c being Surreal
for r, t being Real st a * b == c holds
(a * (uReal . r)) * (b * (uReal . t)) == c * (uReal . (r * t))

proof end;

::Gonshor'86 Lemma 5.6

theorem Th83: :: SURREAL1:83

for A being Ordinal
for a being Surreal
for r being Sequence of REAL
for y being strictly_decreasing Surreal-Sequence st A c= (dom r) /\ (dom y) holds
Sum ((r | A),((No_omega^ (y + a)) | A)) == (No_omega^ a) * (Sum ((r | A),((No_omega^ y) | A)))

proof end;

definition

let S, T be non empty Ordinal;
let y, z be strictly_decreasing Surreal-Sequence;
let r, s be Sequence of REAL ;
let a be Surreal;

func Partial_Sums (y,z,r,s,a,S,T) -> Real equals :: SURREAL1:def 18
addreal $$ (((y,z,S,T) += a),(Product (r,s,S,T)));

coherence
addreal $$ (((y,z,S,T) += a),(Product (r,s,S,T))) is Real ;

end;

:: deftheorem defines Partial_Sums SURREAL1:def 18 :
for S, T being non empty Ordinal
for y, z being strictly_decreasing Surreal-Sequence
for r, s being Sequence of REAL
for a being Surreal holds Partial_Sums (y,z,r,s,a,S,T) = addreal $$ (((y,z,S,T) += a),(Product (r,s,S,T)));

theorem Th84: :: SURREAL1:84

for a being Surreal
for r, s being Sequence of REAL
for y, z being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal st dom y c= S & dom z c= T holds
Partial_Sums (y,z,r,s,a,S,T) = Partial_Sums (z,y,s,r,a,T,S)

proof end;

theorem Th85: :: SURREAL1:85

for a being Surreal
for r1, r2, s being Sequence of REAL
for y, z being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal
for r12 being Sequence of REAL st r1 ^ r2 = r12 & dom y c= dom r1 & dom y c= S & dom z c= T holds
Partial_Sums (y,z,r1,s,a,S,T) = Partial_Sums (y,z,r12,s,a,S,T)

proof end;

theorem Th86: :: SURREAL1:86

for a being Surreal
for r1, r2, r12, s being Sequence of REAL
for y1, y2, y12, z being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal st y1 ^ y2 = y12 & r1 ^ r2 = r12 & dom y12 c= S & dom z c= T & dom y1 = dom r1 & dom y2 c= dom r2 holds
Partial_Sums (y12,z,r12,s,a,S,T) = (Partial_Sums (y1,z,r1,s,a,S,T)) + (Partial_Sums (y2,z,r2,s,a,S,T))

proof end;

registration

let s be Surreal;

cluster <%s%> -> strictly_decreasing ;

coherence
<%s%> is strictly_decreasing

proof end;

end;

theorem Th87: :: SURREAL1:87

for a, b being Surreal
for r, s being Sequence of REAL
for y, z being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal st dom y c= S & dom z c= T & a == b holds
Partial_Sums (y,z,r,s,a,S,T) = Partial_Sums (y,z,r,s,b,S,T)

proof end;

theorem Th88: :: SURREAL1:88

for r, s being Sequence of REAL
for y, z being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal
for c being Surreal st dom y c= S & dom z c= T & ( for a being Surreal st a == c holds
not a in (rng y) ++ (rng z) ) holds
Partial_Sums (y,z,r,s,c,S,T) = 0

proof end;

theorem Th89: :: SURREAL1:89

for A being Ordinal
for a, c being Surreal
for s being Sequence of REAL
for z being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal
for r being Real st dom z c= T & A in dom z & a == c + (z .. A) holds
Partial_Sums (<%c%>,z,<%r%>,s,a,S,T) = r * (s . A)

proof end;

definition

let S, T be non empty Ordinal;
let y, z, yz be strictly_decreasing Surreal-Sequence;
let r, s be Sequence of REAL ;

func Sum (y,z,yz,r,s,S,T) -> Sequence of REAL means :Def19: :: SURREAL1:def 19
( dom it = dom yz & ( for A being Ordinal st A in dom yz holds
it . A = Partial_Sums (y,z,r,s,(yz .. A),S,T) ) );

existence
ex b₁ being Sequence of REAL st
( dom b₁ = dom yz & ( for A being Ordinal st A in dom yz holds
b₁ . A = Partial_Sums (y,z,r,s,(yz .. A),S,T) ) )

proof end;

uniqueness
for b₁, b₂ being Sequence of REAL st dom b₁ = dom yz & ( for A being Ordinal st A in dom yz holds
b₁ . A = Partial_Sums (y,z,r,s,(yz .. A),S,T) ) & dom b₂ = dom yz & ( for A being Ordinal st A in dom yz holds
b₂ . A = Partial_Sums (y,z,r,s,(yz .. A),S,T) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def19 defines Sum SURREAL1:def 19 :
for S, T being non empty Ordinal
for y, z, yz being strictly_decreasing Surreal-Sequence
for r, s, b₈ being Sequence of REAL holds
( b₈ = Sum (y,z,yz,r,s,S,T) iff ( dom b₈ = dom yz & ( for A being Ordinal st A in dom yz holds
b₈ . A = Partial_Sums (y,z,r,s,(yz .. A),S,T) ) ) );

registration

let f be strictly_decreasing Surreal-Sequence;
let A be Ordinal;

cluster f /^ A -> strictly_decreasing ;

coherence
f /^ A is strictly_decreasing

proof end;

end;

theorem Th90: :: SURREAL1:90

for r, s being Sequence of REAL
for y, z, yz being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal st dom y c= S & dom z c= T holds
Sum (y,z,yz,r,s,S,T) = Sum (z,y,yz,s,r,T,S)

proof end;

theorem Th91: :: SURREAL1:91

for r, s being Sequence of REAL
for y, z, yz being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal st y = {} & dom z c= T holds
rng (Sum (y,z,yz,r,s,S,T)) c= {0}

proof end;

theorem Th92: :: SURREAL1:92

for r, s being Sequence of REAL
for y, z, yz being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal
for A, Y, Z being Ordinal st dom y c= S & dom z c= T & A in dom yz & yz .. A > (y .. Y) + (z .. Z) holds
(Sum ((y /^ Y),(z /^ Z),yz,r,s,S,T)) . A = 0

proof end;

theorem Th93: :: SURREAL1:93

for r being Sequence of REAL
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))

proof end;

theorem Th94: :: SURREAL1:94

for A being Ordinal
for r being Sequence of REAL
for y being strictly_decreasing Surreal-Sequence st A c= (dom r) /\ (dom y) holds
Sum ((r | A),((No_omega^ y) | A)) = Sum ((r | A),((No_omega^ (Unique_No y)) | A))

proof end;

theorem Th95: :: SURREAL1:95

for a being Surreal
for s being Sequence of REAL
for z being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal
for yz being strictly_decreasing uSurreal-Sequence
for r being Real st dom s = dom z & dom z c= T & Unique_No ({a} ++ (rng z)) c= rng yz holds
Sum ((Sum (<%a%>,z,yz,<%r%>,s,S,T)),(No_omega^ yz)) == ((uReal . r) * (No_omega^ a)) * (Sum (s,(No_omega^ z)))

proof end;

theorem Th96: :: SURREAL1:96

for a being Surreal
for r being Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal
for yz being strictly_decreasing uSurreal-Sequence
for s being Real st dom r = dom y & dom y c= S & Unique_No ((rng y) ++ {a}) c= rng yz holds
Sum ((Sum (y,<%a%>,yz,r,<%s%>,S,T)),(No_omega^ yz)) == ((uReal . s) * (No_omega^ a)) * (Sum (r,(No_omega^ y)))

proof end;

theorem :: SURREAL1:97

for r, s being Sequence of REAL
for y, z, yz being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal st y = {} & dom z c= T holds
Sum ((Sum (y,z,yz,r,s,S,T)),(No_omega^ yz)) = 0_No

proof end;

theorem Th98: :: SURREAL1:98

for A being Ordinal
for r, s being Sequence of REAL
for y, z, yz being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal st dom y c= S & dom z c= T & dom y c= dom r & A c= dom y holds
(Sum ((y | A),z,yz,(r | A),s,S,T)) + (Sum ((y /^ A),z,yz,(r /^ A),s,S,T)) = Sum (y,z,yz,r,s,S,T)

proof end;

theorem Th99: :: SURREAL1:99

for A being Ordinal
for r, s being Sequence of REAL
for y, z, yz being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal st dom y c= S & dom z c= T & dom y c= dom r & A c= dom y holds
Sum ((Sum (y,z,yz,r,s,S,T)),(No_omega^ yz)) == (Sum ((Sum ((y | A),z,yz,(r | A),s,S,T)),(No_omega^ yz))) + (Sum ((Sum ((y /^ A),z,yz,(r /^ A),s,S,T)),(No_omega^ yz)))

proof end;

theorem Th100: :: SURREAL1:100

for A being Ordinal
for r, s being Sequence of REAL
for y, z, yz being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal st dom y c= S & dom z c= T & dom z c= dom s & A c= dom z holds
Sum ((Sum (y,z,yz,r,s,S,T)),(No_omega^ yz)) == (Sum ((Sum (y,(z | A),yz,r,(s | A),S,T)),(No_omega^ yz))) + (Sum ((Sum (y,(z /^ A),yz,r,(s /^ A),S,T)),(No_omega^ yz)))

proof end;

theorem :: SURREAL1:101

for a being Surreal
for r being Real holds Sum (<%r%>,(No_omega^ <%a%>)) == (uReal . r) * (No_omega^ a)

proof end;

theorem Th102: :: SURREAL1:102

for A being Ordinal
for e being positive Real
for r being Sequence of REAL
for y being strictly_decreasing Surreal-Sequence st succ A c= (dom r) /\ (dom y) holds
( (Sum ((r | A),((No_omega^ y) | A))) + ((uReal . ((r . A) - e)) * ((No_omega^ y) .. A)) == (Sum ((r | (succ A)),((No_omega^ y) | (succ A)))) + ((uReal . (- e)) * (No_omega^ (y .. A))) & (Sum ((r | A),((No_omega^ y) | A))) + ((uReal . ((r . A) + e)) * ((No_omega^ y) .. A)) == (Sum ((r | (succ A)),((No_omega^ y) | (succ A)))) + ((uReal . e) * (No_omega^ (y .. A))) )

proof end;

theorem Th103: :: SURREAL1:103

for x, x0, y, y0, s, t being Surreal holds ((x * (y0 + s)) + ((x0 + t) * y)) - ((x0 + t) * (y0 + s)) == ((((x * y0) + (x0 * y)) - (x0 * y0)) + (((x - x0) * s) + ((y - y0) * t))) - (t * s)

proof end;

Lm7: for r being Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for a being Surreal
for e being positive Real
for A, B being Ordinal st succ B c= A & A c= (dom r) /\ (dom y) holds
|.(((Sum ((r | A),(No_omega^ (y | A)))) - (Sum ((r | (succ B)),(No_omega^ (y | (succ B)))))) * ((uReal . e) * (No_omega^ a))).| infinitely< No_omega^ ((y .. B) + a)

proof end;

theorem Th104: :: SURREAL1:104

for A, B being Ordinal
for a being Surreal
for r being Sequence of REAL
for y being strictly_decreasing Surreal-Sequence
for e being Real st succ B c= A & A c= (dom r) /\ (dom y) holds
|.(((Sum ((r | A),(No_omega^ (y | A)))) - (Sum ((r | (succ B)),(No_omega^ (y | (succ B)))))) * ((uReal . e) * (No_omega^ a))).| infinitely< No_omega^ ((y .. B) + a)

proof end;

theorem Th105: :: SURREAL1:105

for a being Surreal
for r, s being Sequence of REAL
for y, z being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal holds Partial_Sums (y,z,(- r),s,a,S,T) = - (Partial_Sums (y,z,r,s,a,S,T))

proof end;

Lm8: for A, B being non empty Ordinal
for y, z, yz being strictly_decreasing Surreal-Sequence
for r, s being Sequence of REAL holds Sum (y,z,yz,(- r),s,A,B) = - (Sum (y,z,yz,r,s,A,B))

proof end;

theorem :: SURREAL1:106

for r, s being Sequence of REAL
for y, z, yz being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal st dom y c= S & dom z c= T holds
( Sum (y,z,yz,(- r),s,S,T) = - (Sum (y,z,yz,r,s,S,T)) & Sum (y,z,yz,r,(- s),S,T) = - (Sum (y,z,yz,r,s,S,T)) )

proof end;

theorem Th107: :: SURREAL1:107

for A, B being Ordinal
for r, s being Sequence of REAL
for y, z, yz being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal st dom y c= S & dom z c= T & dom y c= dom r & dom z c= dom s & A c= dom y & B c= dom z holds
(Sum ((Sum (y,z,yz,r,s,S,T)),(No_omega^ yz))) - (Sum ((Sum ((y /^ A),(z /^ B),yz,(r /^ A),(s /^ B),S,T)),(No_omega^ yz))) == ((Sum ((Sum ((y | A),z,yz,(r | A),s,S,T)),(No_omega^ yz))) + (Sum ((Sum (y,(z | B),yz,r,(s | B),S,T)),(No_omega^ yz)))) - (Sum ((Sum ((y | A),(z | B),yz,(r | A),(s | B),S,T)),(No_omega^ yz)))

proof end;

theorem Th108: :: SURREAL1:108

for A, B being Ordinal
for a being Surreal
for r, s being Sequence of REAL
for y, z, yz being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal st dom y c= S & dom z c= T & Unique_No ((rng y) ++ (rng z)) c= rng yz & A in dom y & B in dom z & (y .. A) + (z .. B) < a holds
|.(Sum ((Sum ((y /^ A),(z /^ B),yz,r,s,S,T)),(No_omega^ yz))).| infinitely< No_omega^ a

proof end;

theorem Th109: :: SURREAL1:109

for r, s being Sequence of REAL
for y, z being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal
for yz, yzE being strictly_decreasing uSurreal-Sequence st dom y c= S & dom z c= T & Unique_No ((rng y) ++ (rng z)) c= rng yz & rng yz c= rng yzE holds
Sum ((Sum (y,z,yz,r,s,S,T)),(No_omega^ yz)) = Sum ((Sum (y,z,yzE,r,s,S,T)),(No_omega^ yzE))

proof end;

:: Correctness of the Product for Selected Representations
::Gonshor'86 Theorem 5.6

theorem :: SURREAL1:110

for r, s being Sequence of REAL
for y, z being strictly_decreasing Surreal-Sequence
for S, T being non empty Ordinal
for yz being strictly_decreasing uSurreal-Sequence st dom y c= S & dom z c= T & Unique_No ((rng y) ++ (rng z)) c= rng yz & dom y = dom r & dom z = dom s holds
(Sum (r,(No_omega^ y))) * (Sum (s,(No_omega^ z))) == Sum ((Sum (y,z,yz,r,s,S,T)),(No_omega^ yz))

proof end;