let A, B, C be Ordinal; :: thesis: ( A c= B & B in succ C implies (unique_No_op C) . A c= (unique_No_op C) . B )
assume A1: ( A c= B & B in succ C ) ; :: thesis: (unique_No_op C) . A c= (unique_No_op C) . B
set MC = unique_No_op C;
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in (unique_No_op C) . A or o in (unique_No_op C) . B )
assume A2: o in (unique_No_op C) . A ; :: thesis: o in (unique_No_op C) . B
then reconsider x = o as Surreal by SURREAL0:def 16;
set b = born x;
succ C = dom (unique_No_op C) by Def9;
then A3: dom ((unique_No_op C) | B) = B by RELAT_1:62, A1, ORDINAL1:def 2;

per cases ( A = B or A <> B ) ;

suppose A = B ; :: thesis: o in (unique_No_op C) . B

hence o in (unique_No_op C) . B by A2; :: thesis: verum

end;

suppose A <> B ; :: thesis: o in (unique_No_op C) . B

then A4: A in B by ORDINAL1:11, A1, XBOOLE_0:def 8;
then (unique_No_op C) . A = ((unique_No_op C) | B) . A by A3, FUNCT_1:47;
then (unique_No_op C) . A in rng ((unique_No_op C) | B) by A3, A4, FUNCT_1:def 3;
then o in union (rng ((unique_No_op C) | B)) by A2, TARSKI:def 4;
then x in (unique_No_op C) . B by A1, Def9;
hence o in (unique_No_op C) . B ; :: thesis: verum

end;

end;