let f be Function; :: thesis: limit- f = sup (dom f)

per cases ( for a being ordinal number holds a nin dom f or ex a being ordinal number st a in dom f ) ;

suppose A1: for a being ordinal number holds a nin dom f ; :: thesis: limit- f = sup (dom f)

On (dom f) c= 0

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in On (dom f) or x in 0 )
assume x in On (dom f) ; :: thesis: x in 0
then ( x in dom f & x is ordinal ) by ORDINAL1:def 9;
hence x in 0 by A1; :: thesis: verum

end;

then sup (dom f) c= 0 by ORDINAL2:def 3;
then sup (dom f) = 0 ;
hence limit- f = sup (dom f) by A1, LIM; :: thesis: verum

end;

suppose A2: ex a being ordinal number st a in dom f ; :: thesis: limit- f = sup (dom f)

f is sup (dom f) -limited by LI;
hence limit- f = sup (dom f) by A2, LIM; :: thesis: verum

end;

end;