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 :: thesis: for x being set st x in { a where a is Element of dom f : a is_a_fixpoint_of f } holds
x is ordinal

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 Th1;
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 Th2; :: thesis: verum