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 <> {}
now :: thesis: dom fi <> {}
per cases ( A = {} or A <> {} ) ;
suppose A <> {} ; :: thesis: dom fi <> {}
then {} in A by ORDINAL3:8;
then ex B being Ordinal st
( B in dom fi & ( for C being Ordinal st B c= C & C in dom fi holds
( {} in fi . C & fi . C in succ A ) ) ) by A1, ORDINAL1:6;
hence dom fi <> {} ; :: thesis: verum
end;
end;
end;
hence dom fi <> {} ; :: thesis: verum