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 = {} & ex A1 being Ordinal st
( A1 in dom fi & ( for C being Ordinal st A1 c= C & C in dom fi holds
fi . C = {} ) ) ) or ( B <> {} & ( 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 = {} & ex B being Ordinal st
( B in dom psi & ( for A1 being Ordinal st B c= A1 & A1 in dom psi holds
psi . A1 = {} ) ) ) or ( C <> {} & ( 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 13 :: thesis: B c= C

A5: now

let A be Ordinal; :: thesis: ( A in dom fi implies fi . A c= psi . A )
assume A6: A in dom fi ; :: thesis: fi . A c= psi . A
reconsider A1 = fi . A, A2 = psi . A as Ordinal ;
( A1 c= A2 or A1 in A2 ) by A4, A6;
hence fi . A c= psi . A by ORDINAL1:def 2; :: thesis: verum

end;

now

per cases ( ( B = {} & C = {} ) or ( B = {} & C <> {} ) or ( B <> {} & C = {} ) or ( B <> {} & C <> {} ) ) ;

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

hence B c= C ; :: thesis: verum

end;

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

then B in C by ORDINAL3:10;
hence B c= C by ORDINAL1:def 2; :: thesis: verum

end;

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

then consider A1 being Ordinal such that
A8: ( A1 in dom psi & ( for A being Ordinal st A1 c= A & A in dom psi holds
psi . A = {} ) ) by A3;
( {} in B & B in succ B ) by A7, ORDINAL1:10, ORDINAL3:10;
then consider A2 being Ordinal such that
A9: ( A2 in dom fi & ( for A being Ordinal st A2 c= A & A in dom fi holds
( {} in fi . A & fi . A in succ B ) ) ) by A2;
( A1 c= A1 \/ A2 & A2 c= A1 \/ A2 & ( A1 \/ A2 = A1 or A1 \/ A2 = A2 ) ) by ORDINAL3:15, XBOOLE_1:7;
then ( psi . (A1 \/ A2) = {} & {} in fi . (A1 \/ A2) & fi . (A1 \/ A2) c= psi . (A1 \/ A2) ) by A1, A5, A8, A9;
hence B c= C ; :: thesis: verum

end;

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

assume not B c= C ; :: thesis: contradiction
then ( C in B & B in succ B ) by ORDINAL1:10, ORDINAL1:26;
then consider A1 being Ordinal such that
A11: ( A1 in dom fi & ( for A being Ordinal st A1 c= A & A in dom fi holds
( C in fi . A & fi . A in succ B ) ) ) by A2;
( {} in C & C in succ C ) by A10, ORDINAL1:10, ORDINAL3:10;
then consider A2 being Ordinal such that
A12: ( A2 in dom psi & ( for A being Ordinal st A2 c= A & A in dom psi holds
( {} in psi . A & psi . A in succ C ) ) ) by A3;
( A1 c= A1 \/ A2 & A2 c= A1 \/ A2 & ( A1 \/ A2 = A1 or A1 \/ A2 = A2 ) ) by ORDINAL3:15, XBOOLE_1:7;
then A13: ( psi . (A1 \/ A2) in succ C & C in fi . (A1 \/ A2) & A1 \/ A2 in dom psi & fi . (A1 \/ A2) c= psi . (A1 \/ A2) ) by A1, A5, A11, A12;
reconsider A3 = psi . (A1 \/ A2) as Ordinal ;
( A3 c= C & C in A3 ) by A13, ORDINAL1:34;
hence contradiction by ORDINAL1:7; :: thesis: verum

end;

end;

end;

hence B c= C ; :: thesis: verum