let f be Ordinal-Sequence; :: thesis: dom (criticals f) c= dom f
let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in dom (criticals f) or x in dom f )
set X = { a where a is Element of dom f : a is_a_fixpoint_of f } ;
assume A1: x in dom (criticals f) ; :: thesis: x in dom f
then (criticals f) . x in rng (criticals f) by FUNCT_1:def 3;
then (criticals f) . x in On { a where a is Element of dom f : a is_a_fixpoint_of f } by Th18;
then (criticals f) . x in { a where a is Element of dom f : a is_a_fixpoint_of f } by Th28;
then consider a being Element of dom f such that
A2: ( (criticals f) . x = a & a is_a_fixpoint_of f ) ;
( x c= a & a in dom f & a = f . a ) by A1, A2, ORDINAL4:10;
hence x in dom f by ORDINAL1:12; :: thesis: verum