let fi be Ordinal-Sequence; :: thesis: for A being Ordinal st A is_limes_of fi holds

dom fi <> {}

let A be Ordinal; :: thesis: ( A is_limes_of fi implies dom fi <> {} )

assume A1: ( ( A = 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 ( A <> 0 & ( for B, C being Ordinal st B in A & A 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: dom fi <> {}

hence dom fi <> {} ; :: thesis: verum

dom fi <> {}

let A be Ordinal; :: thesis: ( A is_limes_of fi implies dom fi <> {} )

assume A1: ( ( A = 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 ( A <> 0 & ( for B, C being Ordinal st B in A & A 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: dom fi <> {}

hence dom fi <> {} ; :: thesis: verum