let fi be Ordinal-Sequence; :: thesis: for A being Ordinal st dom fi = succ A holds
( last fi is_limes_of fi & lim fi = last fi )
let A be Ordinal; :: thesis: ( dom fi = succ A implies ( last fi is_limes_of fi & lim fi = last fi ) )
assume A1: dom fi = succ A ; :: thesis: ( last fi is_limes_of fi & lim fi = last fi )
then A2: last fi = fi . A by ORDINAL2:6;
thus last fi is_limes_of fi :: thesis: lim fi = last fi
proof
per cases ( last fi = 0 or last fi <> 0 ) ;
:: according to ORDINAL2:def 9
case A3: last fi = 0 ; :: thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or fi . b2 = 0 ) ) )
take A ; :: thesis: ( A in dom fi & ( for b1 being set holds
( not A c= b1 or not b1 in dom fi or fi . b1 = 0 ) ) )
thus A in dom fi by A1, ORDINAL1:6; :: thesis: for b1 being set holds
( not A c= b1 or not b1 in dom fi or fi . b1 = 0 )
let B be Ordinal; :: thesis: ( not A c= B or not B in dom fi or fi . B = 0 )
assume that
A4: A c= B and
A5: B in dom fi ; :: thesis: fi . B = 0
B c= A by A1, A5, ORDINAL1:22;
hence fi . B = 0 by A2, A3, A4, XBOOLE_0:def 10; :: thesis: verum
end;
case last fi <> 0 ; :: thesis: for b1, b2 being set holds
( not b1 in last fi or not last fi in b2 or ex b3 being set st
( b3 in dom fi & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom fi or ( b1 in fi . b4 & fi . b4 in b2 ) ) ) ) )
let B, C be Ordinal; :: thesis: ( not B in last fi or not last fi in C or ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or ( B in fi . b2 & fi . b2 in C ) ) ) ) )
assume that
A6: B in last fi and
A7: last fi in C ; :: thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or ( B in fi . b2 & fi . b2 in C ) ) ) )
take A ; :: thesis: ( A in dom fi & ( for b1 being set holds
( not A c= b1 or not b1 in dom fi or ( B in fi . b1 & fi . b1 in C ) ) ) )
thus A in dom fi by A1, ORDINAL1:6; :: thesis: for b1 being set holds
( not A c= b1 or not b1 in dom fi or ( B in fi . b1 & fi . b1 in C ) )
let D be Ordinal; :: thesis: ( not A c= D or not D in dom fi or ( B in fi . D & fi . D in C ) )
assume that
A8: A c= D and
A9: D in dom fi ; :: thesis: ( B in fi . D & fi . D in C )
D c= A by A1, A9, ORDINAL1:22;
hence ( B in fi . D & fi . D in C ) by A2, A6, A7, A8, XBOOLE_0:def 10; :: thesis: verum
end;
end;
end;
hence lim fi = last fi by ORDINAL2:def 10; :: thesis: verum