let l be limit_ordinal non empty Ordinal; :: thesis: for f being Ordinal-Sequence st f is normal & l in dom (criticals f) holds
(criticals f) . l = Union ((criticals f) | l)
let f be Ordinal-Sequence; :: thesis: ( f is normal & l in dom (criticals f) implies (criticals f) . l = Union ((criticals f) | l) )
set g = criticals f;
reconsider h = (criticals f) | l as increasing Ordinal-Sequence by ORDINAL4:15;
set X = rng h;
assume A0: ( f is normal & l in dom (criticals f) ) ; :: thesis: (criticals f) . l = Union ((criticals f) | l)
then (criticals f) . l is_a_fixpoint_of f by Th02;
then A1: ( (criticals f) . l in dom f & f . ((criticals f) . l) = (criticals f) . l ) by ABIAN:def 3;
A2: l c= dom (criticals f) by A0, ORDINAL1:def 2;
then A3: dom h = l by RELAT_1:62;
A4: for x being set st x in rng h holds
x is_a_fixpoint_of f

proof

let x be set ; :: thesis: ( x in rng h implies x is_a_fixpoint_of f )
assume x in rng h ; :: thesis: x is_a_fixpoint_of f
then consider y being set such that
B1: ( y in dom h & x = h . y ) by FUNCT_1:def 3;
( x = (criticals f) . y & y in dom (criticals f) ) by A2, A3, B1, FUNCT_1:47;
hence x is_a_fixpoint_of f by Th02; :: thesis: verum

end;

reconsider u = union (rng h) as Ordinal ;
S5: h <> {} by A3;

now

let x be set ; :: thesis: ( x in rng h implies x c= (criticals f) . l )
assume x in rng h ; :: thesis: x c= (criticals f) . l
then consider y being set such that
B2: ( y in dom h & x = h . y ) by FUNCT_1:def 3;
( x = (criticals f) . y & y in dom (criticals f) ) by A2, A3, B2, FUNCT_1:47;
then x in (criticals f) . l by A0, A3, B2, ORDINAL2:def 12;
hence x c= (criticals f) . l by ORDINAL1:def 2; :: thesis: verum

end;

then A9: union (rng h) c= (criticals f) . l by ZFMISC_1:76;
then A6: u in dom f by A1, ORDINAL1:12;
u = f . u by A0, A4, S5, A9, Th08, A1, ORDINAL1:12;
then u is_a_fixpoint_of f by A6, ABIAN:def 3;
then consider a being ordinal number such that
A8: ( a in dom (criticals f) & u = (criticals f) . a ) by Th06;
a = l

proof

thus a c= l by A0, A8, A9, ThN4; :: according to XBOOLE_0:def 10 :: thesis: l c= a
let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in l or x in a )
assume C1: x in l ; :: thesis: x in a
then C2: succ x in l by ORDINAL1:28;
then C3: ( (criticals f) . x = h . x & (criticals f) . (succ x) = h . (succ x) & h . (succ x) in rng h ) by A3, C1, FUNCT_1:47, FUNCT_1:def 3;
x in succ x by ORDINAL1:6;
then h . x in h . (succ x) by A3, C2, ORDINAL2:def 12;
then (criticals f) . x in u by C3, TARSKI:def 4;
then ( (criticals f) . a c/= (criticals f) . x & x in dom (criticals f) ) by A2, A8, C1, EXCH1;
then a c/= x by A8, ThN4;
hence x in a by EXCH1; :: thesis: verum

end;

hence (criticals f) . l = Union ((criticals f) | l) by A8; :: thesis: verum