deffunc H1( Ordinal) -> Subset of (Day $1) = Positives $1;
A1: for A, B being Ordinal st A c= B holds
H1(A) c= H1(B) by Th23;
deffunc H2( object , c=-monotone Function-yielding Sequence) -> object = [(Union (divL (||.$1.||,(union (rng $2))))),(Union (divR (||.$1.||,(union (rng $2)))))];
A2: for S being c=-monotone Function-yielding Sequence st ( for A being Ordinal st A in dom S holds
dom (S . A) = H1(A) ) holds
for A being Ordinal
for o being object st o in dom (S . A) holds
H2(o,S | A) = H2(o,S)
proof
let S be c=-monotone Function-yielding Sequence; :: thesis: ( ( for A being Ordinal st A in dom S holds
dom (S . A) = H1(A) ) implies for A being Ordinal
for o being object st o in dom (S . A) holds
H2(o,S | A) = H2(o,S) )
assume A3: for A being Ordinal st A in dom S holds
dom (S . A) = H1(A) ; :: thesis: for A being Ordinal
for o being object st o in dom (S . A) holds
H2(o,S | A) = H2(o,S)
let A be Ordinal; :: thesis: for o being object st o in dom (S . A) holds
H2(o,S | A) = H2(o,S)
let o be object ; :: thesis: ( o in dom (S . A) implies H2(o,S | A) = H2(o,S) )
assume A4: o in dom (S . A) ; :: thesis: H2(o,S | A) = H2(o,S)
S . A <> {} by A4;
then A5: A in dom S by FUNCT_1:def 2;
then A6: dom (S . A) = H1(A) by A3;
then reconsider x = o as Surreal by A4;
set Nx = ||.x.||;
set xx = (L_ ||.x.||) \/ (R_ ||.x.||);
set xxZ = ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No};
A7: ( x in Day A & 0_No < x ) by A6, A4, Def10;
A8: born x c= A by SURREAL0:def 18, A6, A4;
then A9: Positives (born x) c= Positives A by Th23;
A10: x is positive by A6, A4, Def10;
((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= Positives (born x) by A7, Def8, Th24;
then A11: ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= Positives A by A9, XBOOLE_1:1;
A12: dom (S . A) c= dom (union (rng S)) by A5, SURREALR:2;
A13: ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= dom (union (rng (S | A)))
proof
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} or o in dom (union (rng (S | A))) )
assume A14: o in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} ; :: thesis: o in dom (union (rng (S | A)))
then reconsider o = o as Surreal by SURREAL0:def 16;
set b = born o;
((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x) by A10, Th20;
then A15: born o in born x by SURREALO:1, A14;
born o in dom S by A5, A8, A15, ORDINAL1:10;
then A16: born o in dom (S | A) by A15, A8, RELAT_1:57;
then A17: dom ((S | A) . (born o)) c= dom (union (rng (S | A))) by SURREALR:2;
A18: (S | A) . (born o) = S . (born o) by A16, FUNCT_1:47;
A19: o is positive by A10, Th21, A14;
A20: dom (S . (born o)) = H1( born o) by A3, A15, A8, A5, ORDINAL1:10;
o in Day (born o) by SURREAL0:def 18;
then o in H1( born o) by Def10, A19;
hence o in dom (union (rng (S | A))) by A18, A17, A20; :: thesis: verum
end;
A21: ( dom ((union (rng (S | A))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) = ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} & ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} = dom ((union (rng S)) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) ) by A12, A6, A11, XBOOLE_1:1, A13, RELAT_1:62;
for a being object st a in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} holds
((union (rng (S | A))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a = ((union (rng S)) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a
proof
let a be object ; :: thesis: ( a in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} implies ((union (rng (S | A))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a = ((union (rng S)) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a )
assume A22: a in ((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} ; :: thesis: ((union (rng (S | A))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a = ((union (rng S)) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a
then reconsider a = a as Surreal by SURREAL0:def 16;
set b = born a;
A23: ((union (rng (S | A))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a = (union (rng (S | A))) . a by A22, FUNCT_1:49;
A24: ((union (rng S)) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a = (union (rng S)) . a by A22, FUNCT_1:49;
((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No} c= (L_ x) \/ (R_ x) by A10, Th20;
then A25: born a in born x by SURREALO:1, A22;
A26: a is positive by A10, Th21, A22;
A27: dom (S . (born a)) = H1( born a) by A3, A8, A25, A5, ORDINAL1:10;
a in Day (born a) by SURREAL0:def 18;
then ( a in dom (S . (born a)) & born a in A ) by Def10, A26, A27, A25, A8;
hence ((union (rng (S | A))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a = ((union (rng S)) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No})) . a by A23, A24, SURREALR:5; :: thesis: verum
end;
then (union (rng (S | A))) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No}) = (union (rng S)) | (((L_ ||.x.||) \/ (R_ ||.x.||)) \ {0_No}) by A21, FUNCT_1:2;
then ( divL (||.x.||,(union (rng (S | A)))) = divL (||.x.||,(union (rng S))) & divR (||.x.||,(union (rng (S | A)))) = divR (||.x.||,(union (rng S))) ) by Th17;
hence H2(o,S | A) = H2(o,S) ; :: thesis: verum
end;
consider S being c=-monotone Function-yielding Sequence such that
A28: dom S = succ A and
A29: for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of H1(B) st
( S . B = SB & ( for o being object st o in H1(B) holds
SB . o = H2(o,S | B) ) ) from SURREALR:sch 1(A2, A1);
 consider SA being ManySortedSet of H1(A) such that
A30: ( S . A = SA & ( for o being object st o in H1(A) holds
SA . o = H2(o,S | A) ) ) by A29, ORDINAL1:6;
take SA ; :: thesis: ex S being c=-monotone Function-yielding Sequence st
( dom S = succ A & SA = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Positives B st
( S . B = SB & ( for x being object st x in Positives B holds
SB . x = [(Union (divL (||.x.||,(union (rng (S | B)))))),(Union (divR (||.x.||,(union (rng (S | B))))))] ) ) ) )
take S ; :: thesis: ( dom S = succ A & SA = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Positives B st
( S . B = SB & ( for x being object st x in Positives B holds
SB . x = [(Union (divL (||.x.||,(union (rng (S | B)))))),(Union (divR (||.x.||,(union (rng (S | B))))))] ) ) ) )
thus ( dom S = succ A & SA = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Positives B st
( S . B = SB & ( for x being object st x in Positives B holds
SB . x = [(Union (divL (||.x.||,(union (rng (S | B)))))),(Union (divR (||.x.||,(union (rng (S | B))))))] ) ) ) ) by A28, A29, A30; :: thesis: verum