let A1, A2 be Ordinal; :: thesis: ( A1 is_limes_of fi & A2 is_limes_of fi implies A1 = A2 )
assume that
A2: ( ( A1 = 0 & ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = 0 ) ) ) or ( A1 <> 0 & ( for B, C being Ordinal st B in A1 & A1 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
( B in fi . E & fi . E in C ) ) ) ) ) ) and
A3: ( ( A2 = 0 & ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = 0 ) ) ) or ( A2 <> 0 & ( for B, C being Ordinal st B in A2 & A2 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
( B in fi . E & fi . E in C ) ) ) ) ) ) ; :: according to ORDINAL2:def 9 :: thesis: A1 = A2
A4: now :: thesis: not A1 in A2
set x = the Element of A1;
reconsider x = the Element of A1 as Ordinal ;
assume A1 in A2 ; :: thesis: contradiction
then consider D being Ordinal such that
A5: D in dom fi and
A6: for A being Ordinal st D c= A & A in dom fi holds
( A1 in fi . A & fi . A in succ A2 ) by A3, ORDINAL1:6;
now :: thesis: not A1 = 0
assume A1 = 0 ; :: thesis: contradiction
then consider B being Ordinal such that
A7: B in dom fi and
A8: for C being Ordinal st B c= C & C in dom fi holds
fi . C = 0 by A2;
( B c= D or D c= B ) ;
then consider E being Ordinal such that
A9: ( ( E = D & B c= D ) or ( E = B & D c= B ) ) ;
fi . E = 0 by A5, A7, A8, A9;
hence contradiction by A5, A6, A7, A9; :: thesis: verum
end;
then consider C being Ordinal such that
A10: C in dom fi and
A11: for A being Ordinal st C c= A & A in dom fi holds
( x in fi . A & fi . A in succ A1 ) by A2, ORDINAL1:6;
( C c= D or D c= C ) ;
then consider E being Ordinal such that
A12: ( ( E = D & C c= D ) or ( E = C & D c= C ) ) ;
fi . E in succ A1 by A5, A10, A11, A12;
then A13: ( fi . E in A1 or fi . E = A1 ) by ORDINAL1:8;
A1 in fi . E by A5, A6, A10, A12;
hence contradiction by A13; :: thesis: verum
end;
set x = the Element of A2;
reconsider x = the Element of A2 as Ordinal ;
assume A1 <> A2 ; :: thesis: contradiction
then ( A1 in A2 or A2 in A1 ) by ORDINAL1:14;
then consider D being Ordinal such that
A14: D in dom fi and
A15: for A being Ordinal st D c= A & A in dom fi holds
( A2 in fi . A & fi . A in succ A1 ) by A2, A4, ORDINAL1:6;
now :: thesis: not A2 = 0
assume A2 = 0 ; :: thesis: contradiction
then consider B being Ordinal such that
A16: B in dom fi and
A17: for C being Ordinal st B c= C & C in dom fi holds
fi . C = 0 by A3;
( B c= D or D c= B ) ;
then consider E being Ordinal such that
A18: ( ( E = D & B c= D ) or ( E = B & D c= B ) ) ;
fi . E = 0 by A14, A16, A17, A18;
hence contradiction by A14, A15, A16, A18; :: thesis: verum
end;
then consider C being Ordinal such that
A19: C in dom fi and
A20: for A being Ordinal st C c= A & A in dom fi holds
( x in fi . A & fi . A in succ A2 ) by A3, ORDINAL1:6;
( C c= D or D c= C ) ;
then consider E being Ordinal such that
A21: ( ( E = D & C c= D ) or ( E = C & D c= C ) ) ;
fi . E in succ A2 by A14, A19, A20, A21;
then A22: ( fi . E in A2 or fi . E = A2 ) by ORDINAL1:8;
A2 in fi . E by A14, A15, A19, A21;
hence contradiction by A22; :: thesis: verum