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

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

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

On (dom f) c= 0

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in On (dom f) or x in 0 )
reconsider xx = x as set by TARSKI:1;
assume x in On (dom f) ; :: thesis: x in 0
then ( x in dom f & xx 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, Def5; :: thesis: verum

end;

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

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

end;

end;