let f be Ordinal-Sequence; :: thesis: On { a where a is Element of dom f : a is_a_fixpoint_of f } = { a where a is Element of dom f : a is_a_fixpoint_of f }
set X = { a where a is Element of dom f : a is_a_fixpoint_of f } ;

now

let x be set ; :: thesis: ( x in { a where a is Element of dom f : a is_a_fixpoint_of f } implies x is ordinal )
assume x in { a where a is Element of dom f : a is_a_fixpoint_of f } ; :: thesis: x is ordinal
then ex a being Element of dom f st
( x = a & a is_a_fixpoint_of f ) ;
hence x is ordinal ; :: thesis: verum

end;

then { a where a is Element of dom f : a is_a_fixpoint_of f } is ordinal-membered by EXCH9;
hence On { a where a is Element of dom f : a is_a_fixpoint_of f } = { a where a is Element of dom f : a is_a_fixpoint_of f } by EXCH10; :: thesis: verum