let A, B be Ordinal; :: thesis: ( A c= B implies (unique_No_op B) | (succ A) = unique_No_op A )
assume A c= B ; :: thesis: (unique_No_op B) | (succ A) = unique_No_op A
then A1: A in succ B by ORDINAL1:22;
then A2: succ A c= succ B by ORDINAL1:21;
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] } ;
set S1 = unique_No_op A;
set S = unique_No_op B;
set S2 = (unique_No_op B) | (succ A);
A3: dom (unique_No_op A) = succ A by Def9;
A4: dom (unique_No_op B) = succ B by Def9;
then A5: dom ((unique_No_op B) | (succ A)) = succ A by A1, ORDINAL1:21, RELAT_1:62;
A6: ( dom (unique_No_op A) = succ A & ( for B being Ordinal
for L1 being Sequence st B in succ A & L1 = (unique_No_op A) | B holds
(unique_No_op A) . B = H₁(L1) ) )

proof

thus dom (unique_No_op A) = succ A by Def9; :: thesis: for B being Ordinal
for L1 being Sequence st B in succ A & L1 = (unique_No_op A) | B holds
(unique_No_op A) . B = H₁(L1)
let B be Ordinal; :: thesis: for L1 being Sequence st B in succ A & L1 = (unique_No_op A) | B holds
(unique_No_op A) . B = H₁(L1)
let L1 be Sequence; :: thesis: ( B in succ A & L1 = (unique_No_op A) | B implies (unique_No_op A) . B = H₁(L1) )
assume A7: ( B in succ A & L1 = (unique_No_op A) | B ) ; :: thesis: (unique_No_op A) . B = H₁(L1)
A8: dom L1 = B by RELAT_1:62, A3, A7, ORDINAL1:def 2;
A9: (unique_No_op A) . B c= Day B by Def9, A7;
thus (unique_No_op A) . B c= H₁(L1) :: according to XBOOLE_0:def 10 :: thesis: H₁(L1) c= (unique_No_op A) . B

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in (unique_No_op A) . B or o in H₁(L1) )
assume A10: o in (unique_No_op A) . B ; :: thesis: o in H₁(L1)
then reconsider O = o as Surreal by A9;
for x being Surreal st x = o holds
S₁[(unique_No_op A) | B, dom ((unique_No_op A) | B),x] by A10, Def9, A7, A8;
hence o in H₁(L1) by A10, A8, A9, A7; :: thesis: verum

end;

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

end;

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

proof

thus dom ((unique_No_op B) | (succ A)) = succ A by A4, A1, ORDINAL1:21, RELAT_1:62; :: thesis: for C being Ordinal
for L2 being Sequence st C in succ A & L2 = ((unique_No_op B) | (succ A)) | C holds
((unique_No_op B) | (succ A)) . C = H₁(L2)
let C be Ordinal; :: thesis: for L2 being Sequence st C in succ A & L2 = ((unique_No_op B) | (succ A)) | C holds
((unique_No_op B) | (succ A)) . C = H₁(L2)
let L1 be Sequence; :: thesis: ( C in succ A & L1 = ((unique_No_op B) | (succ A)) | C implies ((unique_No_op B) | (succ A)) . C = H₁(L1) )
assume A13: ( C in succ A & L1 = ((unique_No_op B) | (succ A)) | C ) ; :: thesis: ((unique_No_op B) | (succ A)) . C = H₁(L1)
A14: dom L1 = C by RELAT_1:62, A5, A13, ORDINAL1:def 2;
A15: dom ((unique_No_op B) | C) = C by A13, A2, A4, RELAT_1:62, ORDINAL1:def 2;
A16: (unique_No_op B) . C = ((unique_No_op B) | (succ A)) . C by A13, FUNCT_1:49;
A17: ( (unique_No_op B) . C c= Day C & ( for x being Surreal holds
( x in (unique_No_op B) . C iff S₁[(unique_No_op B) | C,C,x] ) ) ) by A13, A2, Def9;
A18: ( ((unique_No_op B) | (succ A)) | C = ((unique_No_op B) | (succ A)) | C & ((unique_No_op B) | (succ A)) | C = (unique_No_op B) | C ) by A13, ORDINAL1:def 2, RELAT_1:74;
thus ((unique_No_op B) | (succ A)) . C c= H₁(L1) :: according to XBOOLE_0:def 10 :: thesis: H₁(L1) c= ((unique_No_op B) | (succ A)) . C

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in ((unique_No_op B) | (succ A)) . C or o in H₁(L1) )
assume A19: o in ((unique_No_op B) | (succ A)) . C ; :: thesis: o in H₁(L1)
then reconsider O = o as Surreal by A16, A17;
for x being Surreal st x = o holds
S₁[((unique_No_op B) | (succ A)) | C, dom (((unique_No_op B) | (succ A)) | C),x] by A18, A16, A19, A15, A13, A2, Def9;
hence o in H₁(L1) by A17, A19, A16, A13, A14; :: thesis: verum

end;

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in H₁(L1) or o in ((unique_No_op B) | (succ A)) . C )
assume o in H₁(L1) ; :: thesis: o in ((unique_No_op B) | (succ A)) . C
then consider e being Element of Day (dom L1) such that
A20: ( o = e & ( for x being Surreal st x = e holds
S₁[L1, dom L1,x] ) ) ;
S₁[(unique_No_op B) | C, dom ((unique_No_op B) | C),e] by A20, A13, A18;
hence o in ((unique_No_op B) | (succ A)) . C by A20, A16, A15, A13, A2, Def9; :: thesis: verum

end;

unique_No_op A = (unique_No_op B) | (succ A) from ORDINAL1:sch 3(A6, A12);
hence (unique_No_op B) | (succ A) = unique_No_op A ; :: thesis: verum