let fi, psi be Ordinal-Sequence; :: thesis: for B, C being Ordinal st dom fi = dom psi & B is_limes_of fi & C is_limes_of psi & ( for A being Ordinal st A in dom fi holds

fi . A c= psi . A or for A being Ordinal st A in dom fi holds

fi . A in psi . A ) holds

B c= C

let B, C be Ordinal; :: thesis: ( dom fi = dom psi & B is_limes_of fi & C is_limes_of psi & ( for A being Ordinal st A in dom fi holds

fi . A c= psi . A or for A being Ordinal st A in dom fi holds

fi . A in psi . A ) implies B c= C )

assume that

A1: dom fi = dom psi and

A2: ( ( B = 0 & ex A1 being Ordinal st

( A1 in dom fi & ( for C being Ordinal st A1 c= C & C in dom fi holds

fi . C = 0 ) ) ) or ( B <> 0 & ( for A1, C being Ordinal st A1 in B & B in C holds

ex D being Ordinal st

( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds

( A1 in fi . E & fi . E in C ) ) ) ) ) ) and

A3: ( ( C = 0 & ex B being Ordinal st

( B in dom psi & ( for A1 being Ordinal st B c= A1 & A1 in dom psi holds

psi . A1 = 0 ) ) ) or ( C <> 0 & ( for B, A1 being Ordinal st B in C & C in A1 holds

ex D being Ordinal st

( D in dom psi & ( for E being Ordinal st D c= E & E in dom psi holds

( B in psi . E & psi . E in A1 ) ) ) ) ) ) and

A4: ( for A being Ordinal st A in dom fi holds

fi . A c= psi . A or for A being Ordinal st A in dom fi holds

fi . A in psi . A ) ; :: according to ORDINAL2:def 9 :: thesis: B c= C

A5: for A being Ordinal st A in dom fi holds

fi . A c= psi . A by A4, ORDINAL1:def 2;

fi . A c= psi . A or for A being Ordinal st A in dom fi holds

fi . A in psi . A ) holds

B c= C

let B, C be Ordinal; :: thesis: ( dom fi = dom psi & B is_limes_of fi & C is_limes_of psi & ( for A being Ordinal st A in dom fi holds

fi . A c= psi . A or for A being Ordinal st A in dom fi holds

fi . A in psi . A ) implies B c= C )

assume that

A1: dom fi = dom psi and

A2: ( ( B = 0 & ex A1 being Ordinal st

( A1 in dom fi & ( for C being Ordinal st A1 c= C & C in dom fi holds

fi . C = 0 ) ) ) or ( B <> 0 & ( for A1, C being Ordinal st A1 in B & B in C holds

ex D being Ordinal st

( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds

( A1 in fi . E & fi . E in C ) ) ) ) ) ) and

A3: ( ( C = 0 & ex B being Ordinal st

( B in dom psi & ( for A1 being Ordinal st B c= A1 & A1 in dom psi holds

psi . A1 = 0 ) ) ) or ( C <> 0 & ( for B, A1 being Ordinal st B in C & C in A1 holds

ex D being Ordinal st

( D in dom psi & ( for E being Ordinal st D c= E & E in dom psi holds

( B in psi . E & psi . E in A1 ) ) ) ) ) ) and

A4: ( for A being Ordinal st A in dom fi holds

fi . A c= psi . A or for A being Ordinal st A in dom fi holds

fi . A in psi . A ) ; :: according to ORDINAL2:def 9 :: thesis: B c= C

A5: for A being Ordinal st A in dom fi holds

fi . A c= psi . A by A4, ORDINAL1:def 2;

now :: thesis: B c= Cend;

hence
B c= C
; :: thesis: verumper cases
( ( B = {} & C = {} ) or ( B = {} & C <> {} ) or ( B <> {} & C = {} ) or ( B <> {} & C <> {} ) )
;

end;

suppose A6:
( B <> {} & C = {} )
; :: thesis: B c= C

then
{} in B
by ORDINAL3:8;

then consider A2 being Ordinal such that

A7: A2 in dom fi and

A8: for A being Ordinal st A2 c= A & A in dom fi holds

( {} in fi . A & fi . A in succ B ) by A2, ORDINAL1:6;

consider A1 being Ordinal such that

A9: A1 in dom psi and

A10: for A being Ordinal st A1 c= A & A in dom psi holds

psi . A = {} by A3, A6;

A11: ( A1 \/ A2 = A1 or A1 \/ A2 = A2 ) by ORDINAL3:12;

then A12: fi . (A1 \/ A2) c= psi . (A1 \/ A2) by A1, A5, A9, A7;

A2 c= A1 \/ A2 by XBOOLE_1:7;

then {} in fi . (A1 \/ A2) by A1, A9, A7, A8, A11;

hence B c= C by A1, A9, A10, A7, A11, A12, XBOOLE_1:7; :: thesis: verum

end;then consider A2 being Ordinal such that

A7: A2 in dom fi and

A8: for A being Ordinal st A2 c= A & A in dom fi holds

( {} in fi . A & fi . A in succ B ) by A2, ORDINAL1:6;

consider A1 being Ordinal such that

A9: A1 in dom psi and

A10: for A being Ordinal st A1 c= A & A in dom psi holds

psi . A = {} by A3, A6;

A11: ( A1 \/ A2 = A1 or A1 \/ A2 = A2 ) by ORDINAL3:12;

then A12: fi . (A1 \/ A2) c= psi . (A1 \/ A2) by A1, A5, A9, A7;

A2 c= A1 \/ A2 by XBOOLE_1:7;

then {} in fi . (A1 \/ A2) by A1, A9, A7, A8, A11;

hence B c= C by A1, A9, A10, A7, A11, A12, XBOOLE_1:7; :: thesis: verum

suppose A13:
( B <> {} & C <> {} )
; :: thesis: B c= C

assume
not B c= C
; :: thesis: contradiction

then C in B by ORDINAL1:16;

then consider A1 being Ordinal such that

A14: A1 in dom fi and

A15: for A being Ordinal st A1 c= A & A in dom fi holds

( C in fi . A & fi . A in succ B ) by A2, ORDINAL1:6;

{} in C by A13, ORDINAL3:8;

then consider A2 being Ordinal such that

A16: A2 in dom psi and

A17: for A being Ordinal st A2 c= A & A in dom psi holds

( {} in psi . A & psi . A in succ C ) by A3, ORDINAL1:6;

A18: ( A1 \/ A2 = A1 or A1 \/ A2 = A2 ) by ORDINAL3:12;

reconsider A3 = psi . (A1 \/ A2) as Ordinal ;

A2 c= A1 \/ A2 by XBOOLE_1:7;

then psi . (A1 \/ A2) in succ C by A1, A14, A16, A17, A18;

then A19: A3 c= C by ORDINAL1:22;

A1 c= A1 \/ A2 by XBOOLE_1:7;

then A20: C in fi . (A1 \/ A2) by A1, A14, A15, A16, A18;

fi . (A1 \/ A2) c= psi . (A1 \/ A2) by A1, A5, A14, A16, A18;

hence contradiction by A20, A19, ORDINAL1:5; :: thesis: verum

end;then C in B by ORDINAL1:16;

then consider A1 being Ordinal such that

A14: A1 in dom fi and

A15: for A being Ordinal st A1 c= A & A in dom fi holds

( C in fi . A & fi . A in succ B ) by A2, ORDINAL1:6;

{} in C by A13, ORDINAL3:8;

then consider A2 being Ordinal such that

A16: A2 in dom psi and

A17: for A being Ordinal st A2 c= A & A in dom psi holds

( {} in psi . A & psi . A in succ C ) by A3, ORDINAL1:6;

A18: ( A1 \/ A2 = A1 or A1 \/ A2 = A2 ) by ORDINAL3:12;

reconsider A3 = psi . (A1 \/ A2) as Ordinal ;

A2 c= A1 \/ A2 by XBOOLE_1:7;

then psi . (A1 \/ A2) in succ C by A1, A14, A16, A17, A18;

then A19: A3 c= C by ORDINAL1:22;

A1 c= A1 \/ A2 by XBOOLE_1:7;

then A20: C in fi . (A1 \/ A2) by A1, A14, A15, A16, A18;

fi . (A1 \/ A2) c= psi . (A1 \/ A2) by A1, A5, A14, A16, A18;

hence contradiction by A20, A19, ORDINAL1:5; :: thesis: verum