let l be limit_ordinal non empty Ordinal; :: thesis: for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & ( for a being ordinal number st a in dom g holds
g . a is normal ) & l in dom (criticals g) holds
(criticals g) . l = Union ((criticals g) | l)
let F be Ordinal-Sequence-valued T-Sequence; :: thesis: ( dom F <> {} & ( for a being ordinal number st a in dom F holds
F . a is normal ) & l in dom (criticals F) implies (criticals F) . l = Union ((criticals F) | l) )
assume AA: dom F <> {} ; :: thesis: ( ex a being ordinal number st
( a in dom F & not F . a is normal ) or not l in dom (criticals F) or (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: ( ( for a being ordinal number st a in dom F holds
F . a is normal ) & l in dom (criticals F) ) ; :: thesis: (criticals F) . l = Union ((criticals F) | l)

A1: now

let a be ordinal number ; :: thesis: ( a in dom F implies ( (criticals F) . l in dom (F . a) & (F . a) . ((criticals F) . l) = (criticals F) . l ) )
set f = F . a;
assume a in dom F ; :: thesis: ( (criticals F) . l in dom (F . a) & (F . a) . ((criticals F) . l) = (criticals F) . l )
then (criticals F) . l is_a_fixpoint_of F . a by A0, ThA2;
hence ( (criticals F) . l in dom (F . a) & (F . a) . ((criticals F) . l) = (criticals F) . l ) by ABIAN:def 3; :: thesis: verum

end;

A2: l c= dom (criticals F) by A0, ORDINAL1:def 2;
then A3: dom h = l by RELAT_1:62;
A4: for a being ordinal number
for x being set st a in dom F & x in rng h holds
x is_a_fixpoint_of F . a

proof

let a be ordinal number ; :: thesis: for x being set st a in dom F & x in rng h holds
x is_a_fixpoint_of F . a
let x be set ; :: thesis: ( a in dom F & x in rng h implies x is_a_fixpoint_of F . a )
assume B0: ( a in dom F & x in rng h ) ; :: thesis: x is_a_fixpoint_of F . a
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 . a by B0, ThA2; :: thesis: verum

end;

reconsider u = union (rng h) as Ordinal ;
T5: 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: u c= (criticals F) . l by ZFMISC_1:76;

now

let c be ordinal number ; :: thesis: ( c in dom F implies u is_a_fixpoint_of F . c )
set f = F . c;
assume D1: c in dom F ; :: thesis: u is_a_fixpoint_of F . c
then A6: (criticals F) . l in dom (F . c) by A1;
then A7: u in dom (F . c) by A9, ORDINAL1:12;
D2: F . c is normal by A0, D1;
for x being set st x in rng h holds
x is_a_fixpoint_of F . c by A4, D1;
then u = (F . c) . u by T5, A6, D2, Th08, A9, ORDINAL1:12;
hence u is_a_fixpoint_of F . c by A7, ABIAN:def 3; :: thesis: verum

end;

then consider a being ordinal number such that
A8: ( a in dom (criticals F) & u = (criticals F) . a ) by AA, ThA6;
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