let a be Ordinal; :: thesis: for l being limit_ordinal non empty Ordinal
for g being Ordinal-Sequence-valued Sequence st dom g <> {} & l c= dom (criticals g) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) & ( for x being set st x in l holds
(criticals g) . x in a ) holds
l in dom (criticals g)
let l be limit_ordinal non empty Ordinal; :: thesis: for g being Ordinal-Sequence-valued Sequence st dom g <> {} & l c= dom (criticals g) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) & ( for x being set st x in l holds
(criticals g) . x in a ) holds
l in dom (criticals g)
let g be Ordinal-Sequence-valued Sequence; :: thesis: ( dom g <> {} & l c= dom (criticals g) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) & ( for x being set st x in l holds
(criticals g) . x in a ) implies l in dom (criticals g) )
set h = criticals g;
assume that
A1: dom g <> {} and
A2: l c= dom (criticals g) and
A3: for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f and
A4: for x being set st x in l holds
(criticals g) . x in a ; :: thesis: l in dom (criticals g)

now :: thesis: for c being Ordinal st c in dom g holds
a is_a_fixpoint_of g . c

let c be Ordinal; :: thesis: ( c in dom g implies a is_a_fixpoint_of g . c )
assume c in dom g ; :: thesis: a is_a_fixpoint_of g . c
then g . c in rng g by FUNCT_1:def 3;
hence a is_a_fixpoint_of g . c by A3; :: thesis: verum

end;

then consider b being Ordinal such that
A5: ( b in dom (criticals g) & a = (criticals g) . b ) by A1, Th50;
l c= b

proof

let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in l or x in b )
assume x in l ; :: thesis: x in b
then ( x in dom (criticals g) & (criticals g) . x in (criticals g) . b ) by A2, A4, A5;
hence x in b by A5, Th23; :: thesis: verum

end;

hence l in dom (criticals g) by A5, ORDINAL1:12; :: thesis: verum