let A1, A2 be Ordinal; :: thesis: ( A1 is_limes_of fi & A2 is_limes_of fi implies A1 = A2 )
assume that
A2: ( ( A1 = {} & ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) ) or ( A1 <> {} & ( 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 = {} & ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) ) or ( A2 <> {} & ( 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 13 :: thesis: A1 = A2
assume A4: A1 <> A2 ; :: thesis: contradiction
then A5: ( A1 in A2 or A2 in A1 ) by ORDINAL1:24;

A6: now

assume A1 in A2 ; :: thesis: contradiction
then consider D being Ordinal such that
A8: D in dom fi and
A9: 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:10;

A10: now

assume A11: A1 = {} ; :: thesis: contradiction
then consider B being Ordinal such that
A12: ( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) by A2;
( B c= D or D c= B ) ;
then consider E being Ordinal such that
A13: ( ( E = D & B c= D ) or ( E = B & D c= B ) ) ;
( fi . E = {} & {} in fi . E ) by A8, A9, A11, A12, A13;
hence contradiction ; :: thesis: verum

end;

consider x being Element of A1;
reconsider x = x as Ordinal ;
consider C being Ordinal such that
A14: C in dom fi and
A15: for A being Ordinal st C c= A & A in dom fi holds
( x in fi . A & fi . A in succ A1 ) by A2, A10, ORDINAL1:10;
( C c= D or D c= C ) ;
then consider E being Ordinal such that
A16: ( ( E = D & C c= D ) or ( E = C & D c= C ) ) ;
A17: ( fi . E in succ A1 & A1 in fi . E ) by A8, A9, A14, A15, A16;
then ( fi . E in A1 or fi . E = A1 ) by ORDINAL1:13;
hence contradiction by A17; :: thesis: verum

end;

then ( A1 in succ A1 & A1 <> {} ) by A4, ORDINAL1:10, ORDINAL1:24;
then consider D being Ordinal such that
A18: D in dom fi and
A19: for A being Ordinal st D c= A & A in dom fi holds
( A2 in fi . A & fi . A in succ A1 ) by A2, A5, A6;

A20: now

assume A21: A2 = {} ; :: thesis: contradiction
then consider B being Ordinal such that
A22: ( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
fi . C = {} ) ) by A3;
( B c= D or D c= B ) ;
then consider E being Ordinal such that
A23: ( ( E = D & B c= D ) or ( E = B & D c= B ) ) ;
( fi . E = {} & {} in fi . E ) by A18, A19, A21, A22, A23;
hence contradiction ; :: thesis: verum

end;

consider x being Element of A2;
reconsider x = x as Ordinal ;
consider C being Ordinal such that
A24: C in dom fi and
A25: for A being Ordinal st C c= A & A in dom fi holds
( x in fi . A & fi . A in succ A2 ) by A3, A20, ORDINAL1:10;
( C c= D or D c= C ) ;
then consider E being Ordinal such that
A26: ( ( E = D & C c= D ) or ( E = C & D c= C ) ) ;
A27: ( fi . E in succ A2 & A2 in fi . E ) by A18, A19, A24, A25, A26;
then ( fi . E in A2 or fi . E = A2 ) by ORDINAL1:13;
hence contradiction by A27; :: thesis: verum