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;
now :: thesis: B c= C
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 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;
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;
end;
end;
hence B c= C ; :: thesis: verum