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