for f being Ordinal-Sequence holds 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 }