defpred S₁[ Sequence, Ordinal, Surreal] means ( $3 in union (rng $1) or ( $2 = born_eq $3 & ex Y being non empty surreal-membered set st
( Y = (born_eq_set $3) /\ (made_of (union (rng $1))) & $3 = the b₁ -smallest Surreal ) ) );
deffunc H₁( Sequence) -> set = { e where e is Element of Day (dom $1) : for x being Surreal st x = e holds
S₁[$1, dom $1,x] } ;
let S1, S2 be Sequence; :: thesis: ( dom S1 = succ A & ( for B being Ordinal st B in succ A holds
( S1 . B c= Day B & ( for x being Surreal holds
( x in S1 . B iff ( x in union (rng (S1 | B)) or ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (S1 | B)))) & x = the b₃ -smallest Surreal ) ) ) ) ) ) ) & dom S2 = succ A & ( for B being Ordinal st B in succ A holds
( S2 . B c= Day B & ( for x being Surreal holds
( x in S2 . B iff ( x in union (rng (S2 | B)) or ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (S2 | B)))) & x = the b₃ -smallest Surreal ) ) ) ) ) ) ) implies S1 = S2 )
assume that
A20: dom S1 = succ A and
A21: for B being Ordinal st B in succ A holds
( S1 . B c= Day B & ( for x being Surreal holds
( x in S1 . B iff S₁[S1 | B,B,x] ) ) ) and
A22: dom S2 = succ A and
A23: for B being Ordinal st B in succ A holds
( S2 . B c= Day B & ( for x being Surreal holds
( x in S2 . B iff S₁[S2 | B,B,x] ) ) ) ; :: thesis: S1 = S2
A24: ( dom S1 = succ A & ( for B being Ordinal
for L1 being Sequence st B in succ A & L1 = S1 | B holds
S1 . B = H₁(L1) ) )

proof

thus dom S1 = succ A by A20; :: thesis: for B being Ordinal
for L1 being Sequence st B in succ A & L1 = S1 | B holds
S1 . B = H₁(L1)
let B be Ordinal; :: thesis: for L1 being Sequence st B in succ A & L1 = S1 | B holds
S1 . B = H₁(L1)
let L1 be Sequence; :: thesis: ( B in succ A & L1 = S1 | B implies S1 . B = H₁(L1) )
assume A25: ( B in succ A & L1 = S1 | B ) ; :: thesis: S1 . B = H₁(L1)
A26: dom L1 = B by RELAT_1:62, A20, A25, ORDINAL1:def 2;
A27: S1 . B c= Day B by A21, A25;
thus S1 . B c= H₁(L1) :: according to XBOOLE_0:def 10 :: thesis: H₁(L1) c= S1 . B

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in S1 . B or o in H₁(L1) )
assume A28: o in S1 . B ; :: thesis: o in H₁(L1)
then reconsider O = o as Surreal by A27;
for x being Surreal st x = o holds
S₁[S1 | B, dom (S1 | B),x] by A28, A21, A25, A26;
hence o in H₁(L1) by A25, A28, A27, A26; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in H₁(L1) or o in S1 . B )
assume o in H₁(L1) ; :: thesis: o in S1 . B
then consider e being Element of Day (dom L1) such that
A29: ( o = e & ( for x being Surreal st x = e holds
S₁[L1, dom L1,x] ) ) ;
S₁[L1, dom L1,e] by A29;
hence o in S1 . B by A29, A21, A25, A26; :: thesis: verum

end;

A30: ( dom S2 = succ A & ( for B being Ordinal
for L2 being Sequence st B in succ A & L2 = S2 | B holds
S2 . B = H₁(L2) ) )

proof

thus dom S2 = succ A by A22; :: thesis: for B being Ordinal
for L2 being Sequence st B in succ A & L2 = S2 | B holds
S2 . B = H₁(L2)
let B be Ordinal; :: thesis: for L2 being Sequence st B in succ A & L2 = S2 | B holds
S2 . B = H₁(L2)
let L1 be Sequence; :: thesis: ( B in succ A & L1 = S2 | B implies S2 . B = H₁(L1) )
assume A31: ( B in succ A & L1 = S2 | B ) ; :: thesis: S2 . B = H₁(L1)
A32: dom L1 = B by RELAT_1:62, A22, A31, ORDINAL1:def 2;
A33: S2 . B c= Day B by A23, A31;
thus S2 . B c= H₁(L1) :: according to XBOOLE_0:def 10 :: thesis: H₁(L1) c= S2 . B

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in S2 . B or o in H₁(L1) )
assume A34: o in S2 . B ; :: thesis: o in H₁(L1)
then reconsider O = o as Surreal by A33;
for x being Surreal st x = o holds
S₁[S2 | B, dom (S2 | B),x] by A34, A23, A31, A32;
hence o in H₁(L1) by A31, A34, A33, A32; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in H₁(L1) or o in S2 . B )
assume o in H₁(L1) ; :: thesis: o in S2 . B
then consider e being Element of Day (dom L1) such that
A35: ( o = e & ( for x being Surreal st x = e holds
S₁[L1, dom L1,x] ) ) ;
S₁[L1, dom L1,e] by A35;
hence o in S2 . B by A35, A23, A31, A32; :: thesis: verum

end;

S1 = S2 from ORDINAL1:sch 3(A24, A30);
hence S1 = S2 ; :: thesis: verum