let x be set ; :: thesis: for f being Ordinal-Sequence st x in dom (criticals f) holds
(criticals f) . x is_a_fixpoint_of f
let f be Ordinal-Sequence; :: thesis: ( x in dom (criticals f) implies (criticals f) . x is_a_fixpoint_of f )
set a = x;
set X = { b where b is Element of dom f : b is_a_fixpoint_of f } ;
set g = criticals f;
assume x in dom (criticals f) ; :: thesis: (criticals f) . x is_a_fixpoint_of f
then (criticals f) . x in rng (criticals f) by FUNCT_1:def 3;
then (criticals f) . x in On { b where b is Element of dom f : b is_a_fixpoint_of f } by Th18;
then (criticals f) . x in { b where b is Element of dom f : b is_a_fixpoint_of f } by Th28;
then ex b being Element of dom f st
( (criticals f) . x = b & b is_a_fixpoint_of f ) ;
hence (criticals f) . x is_a_fixpoint_of f ; :: thesis: verum